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 )
;

end;

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;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