let T be TopStruct ; :: thesis: ( T is empty implies T is connected )
assume A1: T is empty ; :: thesis: T is connected
let A be Subset of T; :: according to CONNSP_1:def 2 :: thesis: for b₁ being Element of bool the carrier of T holds
( not [#] T = A \/ b₁ or not A,b₁ are_separated or A = {} T or b₁ = {} T )
reconsider T = T as empty TopStruct by A1;
the carrier of T is empty ;
hence for b₁ being Element of bool the carrier of T holds
( not [#] T = A \/ b₁ or not A,b₁ are_separated or A = {} T or b₁ = {} T ) ; :: thesis: verum