consider T being non empty TopSpace;
take T_1-reflex T ; :: thesis: ( T_1-reflex T is T_1 & not T_1-reflex T is empty )
thus ( T_1-reflex T is T_1 & not T_1-reflex T is empty ) ; :: thesis: verum