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 & A is connected ) ; :: thesis: B is connected

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 & A is connected ) ; :: thesis: B is connected

now :: thesis: for P, Q being Subset of T st B = P \/ Q & P,Q are_separated & not P = {} T holds

Q = {} T

hence
B is connected
by CONNSP_1:15; :: thesis: verumQ = {} T

let P, Q be Subset of T; :: thesis: ( B = P \/ Q & P,Q are_separated & not P = {} T implies Q = {} T )

assume that

A3: B = P \/ Q and

A4: 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, A4, Th5;

then ( P1 = {} S or Q1 = {} S ) by A2, A3, CONNSP_1:15;

hence ( P = {} T or Q = {} T ) ; :: thesis: verum

end;assume that

A3: B = P \/ Q and

A4: 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, A4, Th5;

then ( P1 = {} S or Q1 = {} S ) by A2, A3, CONNSP_1:15;

hence ( P = {} T or Q = {} T ) ; :: thesis: verum