let T be TopSpace; :: thesis: ( TopStruct(# the carrier of T,the topology of T #) is connected implies T is connected )
set G = TopStruct(# the carrier of T,the topology of T #);
assume A1: TopStruct(# the carrier of T,the topology of T #) is connected ; :: thesis: T is connected
let A, B be Subset of T; :: according to CONNSP_1:def 2 :: thesis: ( not [#] T = A \/ B or not A,B are_separated or A = {} T or B = {} T )
assume that
A2: [#] T = A \/ B and
A3: A,B are_separated ; :: thesis: ( A = {} T or B = {} T )
reconsider A1 = A, B1 = B as Subset of TopStruct(# the carrier of T,the topology of T #) ;
A4: [#] TopStruct(# the carrier of T,the topology of T #) = A1 \/ B1 by A2;
A1,B1 are_separated by A3, Th7;
then ( A1 = {} TopStruct(# the carrier of T,the topology of T #) or B1 = {} TopStruct(# the carrier of T,the topology of T #) ) by A1, A4, CONNSP_1:def 2;
hence ( A = {} T or B = {} T ) ; :: thesis: verum