let S be Subset of FT; :: thesis: ( S is empty implies S is connected )
assume A1: S is empty ; :: thesis: S is connected
let B, C be Subset of FT; :: according to FIN_TOPO:def 16 :: thesis: ( not S = B \/ C or B = {} or C = {} or not B misses C or not B ^b misses C )
assume that
A2: ( S = B \/ C & B <> {} ) and
C <> {} and
B misses C ; :: thesis: not B ^b misses C
thus not B ^b misses C by A1, A2; :: thesis: verum