let T be TopSpace; :: thesis: ( T is T_1/2 implies T is T_0 )

per cases ( not T is empty or T is empty ) ;

suppose not T is empty ; :: thesis: ( T is T_1/2 implies T is T_0 )

then reconsider T9 = T as non empty TopSpace ;
assume T is T_1/2 ; :: thesis: T is T_0
then T9 is T_1/2 ;
hence T is T_0 by Th47; :: thesis: verum

end;

suppose T is empty ; :: thesis: ( T is T_1/2 implies T is T_0 )

then reconsider T9 = T as empty TopSpace ;
T9 is T_0 ;
hence ( T is T_1/2 implies T is T_0 ) ; :: thesis: verum

end;

end;