let X be non empty TopSpace; :: thesis:
let X1, X2 be non empty SubSpace of X; :: thesis:
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
thus ( X1,X2 are_separated implies ex Y1, Y2 being non empty open SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ) ) :: thesis:

assume X1,X2 are_separated ; :: thesis:
then A1,A2 are_separated ;
then consider C1, C2 being Subset of X such that
A1: A1 c= C1 and
A2: A2 c= C2 and
A3: C1 /\ C2 misses A1 \/ A2 and
A4: C1 is open and
A5: C2 is open by Th45;
not C1 is empty by A1, XBOOLE_1:3;
then consider Y1 being non empty strict open SubSpace of X such that
A6: C1 = the carrier of Y1 by A4, Th20;
not C2 is empty by A2, XBOOLE_1:3;
then consider Y2 being non empty strict open SubSpace of X such that
A7: C2 = the carrier of Y2 by A5, Th20;
take Y1 ; :: thesis:
take Y2 ; :: thesis:

end;

hence ( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ) by A1, A2, A6, A7, Th4; :: thesis:

end;

given Y1, Y2 being non empty open SubSpace of X such that A9: ( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 ) and
A10: ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ; :: thesis:

let A1, A2 be Subset of X; :: thesis:
assume A11: ( A1 = the carrier of X1 & A2 = the carrier of X2 ) ; :: thesis:
ex C1, C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 & C1 is open & C2 is open )

reconsider C2 = the carrier of Y2 as Subset of X by Th1;
reconsider C1 = the carrier of Y1 as Subset of X by Th1;
take C1 ; :: thesis:
take C2 ; :: thesis:

end;

end;

hence ( A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 & C1 is open & C2 is open ) by A9, A11, Th4, Th16; :: thesis:

end;

end;