let T be non empty TopSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum