let T be non empty TopSpace; :: thesis: for p being Point of T holds (T_0-canonical_map T) . p = Class ((Indiscernibility T),p)
let p be Point of T; :: thesis: (T_0-canonical_map T) . p = Class ((Indiscernibility T),p)
set F = T_0-canonical_map T;
set R = Indiscernibility T;
(T_0-canonical_map T) . p in the carrier of (T_0-reflex T) ;
then (T_0-canonical_map T) . p in Indiscernible T by BORSUK_1:def 7;
then consider y being Element of T such that
A1: (T_0-canonical_map T) . p = Class ((Indiscernibility T),y) by EQREL_1:36;
p in Class ((Indiscernibility T),y) by A1, BORSUK_1:28;
hence (T_0-canonical_map T) . p = Class ((Indiscernibility T),p) by A1, EQREL_1:23; :: thesis: verum