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
now :: thesis: for P, Q being Subset of T st B = P \/ Q & P,Q are_separated & not P = {} T holds
Q = {} 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;
hence B is connected by CONNSP_1:15; :: thesis: verum