let T be non empty TopSpace; for A being Subset of T st A is open holds
for p, q being Point of T st p in A & (T_0-canonical_map T) . p = (T_0-canonical_map T) . q holds
q in A
let A be Subset of T; ( A is open implies for p, q being Point of T st p in A & (T_0-canonical_map T) . p = (T_0-canonical_map T) . q holds
q in A )
assume A1:
A is open
; for p, q being Point of T st p in A & (T_0-canonical_map T) . p = (T_0-canonical_map T) . q holds
q in A
set F = T_0-canonical_map T;
let p, q be Point of T; ( p in A & (T_0-canonical_map T) . p = (T_0-canonical_map T) . q implies q in A )
assume that
A2:
p in A
and
A3:
(T_0-canonical_map T) . p = (T_0-canonical_map T) . q
; q in A
A4:
(T_0-canonical_map T) . p = Class ((Indiscernibility T),p)
by Th4;
q in (T_0-canonical_map T) . p
by A3, BORSUK_1:28;
then
[q,p] in Indiscernibility T
by A4, EQREL_1:19;
hence
q in A
by A1, A2, Def3; verum