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) )

hereby :: thesis: ( ex p being Point of T st C = Class ((Indiscernibility T),p) implies 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;

assume ex p being Point of T st C = Class ((Indiscernibility T),p) ; :: thesis: C is Point of (T_0-reflex T)
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