let T be non empty TopSpace; :: thesis: for C being set holds

( C is Point of (T_0-reflex T) iff ex p being Point of T st C = Class ((Indiscernibility T),p) )

set TR = T_0-reflex T;

set R = Indiscernibility T;

let C be set ; :: thesis: ( C is Point of (T_0-reflex T) iff ex p being Point of T st C = Class ((Indiscernibility T),p) )

then C in Class (Indiscernibility T) by EQREL_1:def 3;

hence C is Point of (T_0-reflex T) by BORSUK_1:def 7; :: thesis: verum

( C is Point of (T_0-reflex T) iff ex p being Point of T st C = Class ((Indiscernibility T),p) )

set TR = T_0-reflex T;

set R = Indiscernibility T;

let C be set ; :: thesis: ( C is Point of (T_0-reflex T) iff ex p being Point of T st C = Class ((Indiscernibility T),p) )

hereby :: thesis: ( ex p being Point of T st C = Class ((Indiscernibility T),p) implies C is Point of (T_0-reflex T) )

assume
ex p being Point of T st C = Class ((Indiscernibility T),p)
; :: thesis: C is Point of (T_0-reflex T)assume
C is Point of (T_0-reflex T)
; :: thesis: ex p being Point of T st C = Class ((Indiscernibility T),p)

then C in the carrier of (T_0-reflex T) ;

then C in Indiscernible T by BORSUK_1:def 7;

hence ex p being Point of T st C = Class ((Indiscernibility T),p) by EQREL_1:36; :: thesis: verum

end;then C in the carrier of (T_0-reflex T) ;

then C in Indiscernible T by BORSUK_1:def 7;

hence ex p being Point of T st C = Class ((Indiscernibility T),p) by EQREL_1:36; :: thesis: verum

then C in Class (Indiscernibility T) by EQREL_1:def 3;

hence C is Point of (T_0-reflex T) by BORSUK_1:def 7; :: thesis: verum