set T = the non empty TopSpace;
take T_1-reflex the non empty TopSpace ; :: thesis: ( T_1-reflex the non empty TopSpace is T_1 & not T_1-reflex the non empty TopSpace is empty )
thus ( T_1-reflex the non empty TopSpace is T_1 & not T_1-reflex the non empty TopSpace is empty ) ; :: thesis: verum