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 closed SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 ) ) :: 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 misses A2 & C2 misses A1 ) and
A4: C1 is closed and
A5: C2 is closed by Th42;
not C1 is empty by A1, XBOOLE_1:3;
then consider Y1 being non empty strict closed SubSpace of X such that
A6: C1 = the carrier of Y1 by A4, Th15;
not C2 is empty by A2, XBOOLE_1:3;
then consider Y2 being non empty strict closed SubSpace of X such that
A7: C2 = the carrier of Y2 by A5, Th15;
take Y1 ; :: thesis:
take Y2 ; :: thesis:
thus ( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 ) by A1, A2, A3, A6, A7, Th4; :: thesis:

end;

given Y1, Y2 being non empty closed SubSpace of X such that A8: ( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 ) ; :: thesis:

let A1, A2 be Subset of X; :: thesis:
assume A9: ( 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 misses A2 & C2 misses A1 & C1 is closed & C2 is closed )

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:
thus ( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed ) by A8, A9, Th4, Th11; :: thesis:

end;

end;