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;

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

( (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
[q,p] in Indiscernibility T
; :: thesis: (T_0-canonical_map T) . q = (T_0-canonical_map T) . passume
(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;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

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