take 1TopSp {0} ; :: thesis: ( 1TopSp {0} is compact & 1TopSp {0} is T_2 )
thus ( 1TopSp {0} is compact & 1TopSp {0} is T_2 ) ; :: thesis: verum