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 #); :: according to CONNSP_1:def 2 :: thesis: ( 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 that
A1: [#] TopStruct(# the carrier of T,the topology of T #) = A \/ B and
A2: A,B are_separated ; :: thesis: ( 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 ;
A3: [#] T = A1 \/ B1 by A1;
A1,B1 are_separated by A2, Th7;
then ( A1 = {} T or B1 = {} T ) by A3, 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 #) ) ; :: thesis: verum