let S, T be TopSpace; :: thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is connected implies T is connected )

assume that

A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and

A2: S 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

A3: [#] T = A \/ B and

A4: A,B are_separated ; :: thesis: ( A = {} T or B = {} T )

reconsider A1 = A, B1 = B as Subset of S by A1;

( [#] S = the carrier of S & A1,B1 are_separated ) by A1, A4, Th5;

then ( A1 = {} S or B1 = {} S ) by A1, A2, A3;

hence ( A = {} T or B = {} T ) ; :: thesis: verum

assume that

A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and

A2: S 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

A3: [#] T = A \/ B and

A4: A,B are_separated ; :: thesis: ( A = {} T or B = {} T )

reconsider A1 = A, B1 = B as Subset of S by A1;

( [#] S = the carrier of S & A1,B1 are_separated ) by A1, A4, Th5;

then ( A1 = {} S or B1 = {} S ) by A1, A2, A3;

hence ( A = {} T or B = {} T ) ; :: thesis: verum