let T be non empty TopSpace; :: thesis: for p, q being Point of T holds
( (T_0-canonical_map T) . q = (T_0-canonical_map T) . p iff [q,p] in Indiscernibility T )
let p, q be Point of T; :: thesis: ( (T_0-canonical_map T) . q = (T_0-canonical_map T) . p iff [q,p] in Indiscernibility T )
set F = T_0-canonical_map T;
set R = Indiscernibility T;

hereby :: thesis: ( [q,p] in Indiscernibility T implies (T_0-canonical_map T) . q = (T_0-canonical_map T) . p )

assume (T_0-canonical_map T) . q = (T_0-canonical_map T) . p ; :: thesis: [q,p] in Indiscernibility T
then q in (T_0-canonical_map T) . p by BORSUK_1:28;
then q in Class ((Indiscernibility T),p) by Th4;
hence [q,p] in Indiscernibility T by EQREL_1:19; :: thesis: verum

end;

assume [q,p] in Indiscernibility T ; :: thesis: (T_0-canonical_map T) . q = (T_0-canonical_map T) . p
then Class ((Indiscernibility T),q) = Class ((Indiscernibility T),p) by EQREL_1:35;
then (T_0-canonical_map T) . q = Class ((Indiscernibility T),p) by Th4;
hence (T_0-canonical_map T) . q = (T_0-canonical_map T) . p by Th4; :: thesis: verum