consider T being non empty TopSpace;
take T_0-reflex T ; :: thesis: ( T_0-reflex T is T_0 & not T_0-reflex T is empty )
for x, y being Point of (T_0-reflex T) st x <> y holds
ex V being Subset of (T_0-reflex T) st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) by Lm1;
hence ( T_0-reflex T is T_0 & not T_0-reflex T is empty ) by Def7; :: thesis: verum