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: ( [#] (T | C) = A \/ B & A,B are_separated & not A = {} (T | C) implies 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

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: ( [#] (T | C) = A \/ B & A,B are_separated & not A = {} (T | C) implies 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