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 closed 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 closed SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 ) )
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: ( 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 ) implies X1,X2 are_separated )

proof

assume X1,X2 are_separated ; :: thesis: 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 )
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: ex 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 )
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, A3, A6, A7, Th4; :: thesis: verum

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: X1,X2 are_separated

now :: thesis: for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_separated

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 closed & C2 is closed )

proof

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: ex C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed )
take C2 ; :: thesis: ( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed )
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: verum

end;

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

end;

hence X1,X2 are_separated ; :: thesis: verum