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

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