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

now

assume not Y1 misses Y2 ; :: thesis: Y1 meet Y2 misses X1 union X2
then A7: the carrier of (Y1 meet Y2) = C1 /\ C2 by A5, A6, Def5;
the carrier of (X1 union X2) = A1 \/ A2 by Def2;
hence Y1 meet Y2 misses X1 union X2 by A2, A7, Def3; :: thesis: verum

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, A5, A6, 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 ) and
A9: ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ; :: 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 A10: ( 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 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed )

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 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed )
take C2 ; :: thesis: ( A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed )

now

per cases ( Y1 misses Y2 or not Y1 misses Y2 ) ;

suppose Y1 misses Y2 ; :: thesis: C1 /\ C2 misses A1 \/ A2

then C1 misses C2 by Def3;
then C1 /\ C2 = {} by XBOOLE_0:def 7;
hence C1 /\ C2 misses A1 \/ A2 by XBOOLE_1:65; :: thesis: verum

end;

suppose A11: not Y1 misses Y2 ; :: thesis: C1 /\ C2 misses A1 \/ A2

then ( the carrier of (Y1 meet Y2) = C1 /\ C2 & the carrier of (X1 union X2) = A1 \/ A2 ) by A10, Def2, Def5;
hence C1 /\ C2 misses A1 \/ A2 by A9, A11, Def3; :: thesis: verum

end;

end;

end;

hence ( A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed ) by A8, A10, Th4, Th11; :: thesis: verum

end;

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

end;

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