set T = the non empty TopSpace;
take T_0-reflex the non empty TopSpace ; :: thesis: ( T_0-reflex the non empty TopSpace is T_0 & not T_0-reflex the non empty TopSpace is empty )
for x, y being Point of (T_0-reflex the non empty TopSpace) st x <> y holds
ex V being Subset of (T_0-reflex the non empty TopSpace) 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 the non empty TopSpace is T_0 & not T_0-reflex the non empty TopSpace is empty ) ; :: thesis: verum