let T be non empty TopSpace; :: thesis: T_0-reflex T is T_0-TopSpace

for x, y being Point of (T_0-reflex T) st not x = y holds

ex A being Subset of (T_0-reflex T) st

( A is open & ( ( x in A & not y in A ) or ( y in A & not x in A ) ) ) by Lm1;

hence T_0-reflex T is T_0-TopSpace by Def7; :: thesis: verum

for x, y being Point of (T_0-reflex T) st not x = y holds

ex A being Subset of (T_0-reflex T) st

( A is open & ( ( x in A & not y in A ) or ( y in A & not x in A ) ) ) by Lm1;

hence T_0-reflex T is T_0-TopSpace by Def7; :: thesis: verum