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