let S, T be TopSpace; :: thesis: for A being Subset of S
for B being Subset of T st TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & A = B & A is connected holds
B is connected
let A be Subset of S; :: thesis: for B being Subset of T st TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & A = B & A is connected holds
B is connected
let B be Subset of T; :: thesis: ( TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & A = B & A is connected implies B 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: A = B and
A3: A is connected ; :: thesis: B is connected

now

let P, Q be Subset of T; :: thesis: ( B = P \/ Q & P,Q are_separated & not P = {} T implies Q = {} T )
assume that
A4: B = P \/ Q and
A5: P,Q are_separated ; :: thesis: ( P = {} T or Q = {} T )
reconsider P1 = P, Q1 = Q as Subset of S by A1;
P1,Q1 are_separated by A1, A5, Th5;
then ( P1 = {} S or Q1 = {} S ) by A2, A3, A4, CONNSP_1:16;
hence ( P = {} T or Q = {} T ) ; :: thesis: verum

end;

hence B is connected by CONNSP_1:16; :: thesis: verum