let X be non empty TopSpace; :: thesis: for X1, X2 being non empty SubSpace of X holds
( X1,X2 are_separated iff ex Y1, Y2 being non empty open SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 ) )
let X1, X2 be non empty SubSpace of X; :: thesis: ( X1,X2 are_separated iff ex Y1, Y2 being non empty open SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 ) )
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 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 X2 & Y2 misses X1 ) ) :: thesis: ( ex Y1, Y2 being non empty open SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 ) implies X1,X2 are_separated )

proof

assume X1,X2 are_separated ; :: thesis: ex Y1, Y2 being non empty open SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 )
then A1,A2 are_separated by Def8;
then consider C1, C2 being Subset of X such that
A1: ( A1 c= C1 & A2 c= C2 ) and
A2: ( C1 misses A2 & C2 misses A1 ) and
A3: ( C1 is open & C2 is open ) by Th48;
A4: ( not C1 is empty & not C2 is empty ) by A1, XBOOLE_1:3;
then consider Y1 being non empty strict open SubSpace of X such that
A5: C1 = the carrier of Y1 by A3, Th20;
consider Y2 being non empty strict open SubSpace of X such that
A6: C2 = the carrier of Y2 by A3, A4, Th20;
take Y1 ; :: thesis: ex Y2 being non empty open SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 )
take Y2 ; :: thesis: ( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 )
thus ( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 ) by A1, A2, A5, A6, Def3, Th4; :: thesis: verum

end;

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

now

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

proof

reconsider C1 = the carrier of Y1 as Subset of X by Th1;
reconsider C2 = the carrier of Y2 as Subset of X by Th1;
take C1 ; :: thesis: ex C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is open & C2 is open )
take C2 ; :: thesis: ( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is open & C2 is open )
thus ( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is open & C2 is open ) by A7, A8, A9, Def3, Th4, Th16; :: thesis: verum

end;

hence A1,A2 are_separated by Th48; :: thesis: verum

end;

hence X1,X2 are_separated by Def8; :: thesis: verum