let C be Subset of T; :: thesis: ( C is empty implies C is connected )
assume C is empty ; :: thesis: C is connected
then reconsider D = C as empty Subset of T ;
let A, B be Subset of (T | C); :: according to CONNSP_1:def 2,CONNSP_1:def 3 :: thesis: ( not [#] (T | C) = A \/ B or not A,B are_separated or A = {} (T | C) or B = {} (T | C) )
assume that
[#] (T | C) = A \/ B and
A,B are_separated ; :: thesis: ( A = {} (T | C) or B = {} (T | C) )
[#] (T | D) = {} ;
hence ( A = {} (T | C) or B = {} (T | C) ) ; :: thesis: verum