set G = TopStruct(# the carrier of T, the topology of T #);
let A, B be Subset of TopStruct(# the carrier of T, the topology of T #); CONNSP_1:def 2 ( not [#] TopStruct(# the carrier of T, the topology of T #) = A \/ B or not A,B are_separated or A = {} TopStruct(# the carrier of T, the topology of T #) or B = {} TopStruct(# the carrier of T, the topology of T #) )
assume A1:
( [#] TopStruct(# the carrier of T, the topology of T #) = A \/ B & A,B are_separated )
; ( A = {} TopStruct(# the carrier of T, the topology of T #) or B = {} TopStruct(# the carrier of T, the topology of T #) )
reconsider A1 = A, B1 = B as Subset of T ;
( [#] T = A1 \/ B1 & A1,B1 are_separated )
by A1, Th6;
then
( A1 = {} T or B1 = {} T )
by CONNSP_1:def 2;
hence
( A = {} TopStruct(# the carrier of T, the topology of T #) or B = {} TopStruct(# the carrier of T, the topology of T #) )
; verum