let S, T be TopSpace; :: thesis: for A, B being Subset of T
for C, D being Subset of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = C & B = D & A,B are_separated holds
C,D are_separated
let A, B be Subset of T; :: thesis: for C, D being Subset of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = C & B = D & A,B are_separated holds
C,D are_separated
let C, D be Subset of S; :: thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = C & B = D & A,B are_separated implies C,D are_separated )
assume A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) ; :: thesis: ( not A = C or not B = D or not A,B are_separated or C,D are_separated )
assume A2: ( A = C & B = D ) ; :: thesis: ( not A,B are_separated or C,D are_separated )
assume A,B are_separated ; :: thesis: C,D are_separated
then A3: ( Cl A misses B & A misses Cl B ) by CONNSP_1:def 1;
( Cl A = Cl C & Cl B = Cl D ) by A1, A2, TOPS_3:80;
hence C,D are_separated by A2, A3, CONNSP_1:def 1; :: thesis: verum