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 10;
hence ex p being Point of T st C = Class (Indiscernibility T),p by EQREL_1:45; :: 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 5;
hence C is Point of (T_0-reflex T) by BORSUK_1:def 10; :: thesis: verum