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