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