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 SubSpace of X st
( Y1,Y2 are_weakly_separated & 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 SubSpace of X st
( Y1,Y2 are_weakly_separated & X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ) )
thus ( X1,X2 are_separated implies ex Y1, Y2 being non empty SubSpace of X st
( Y1,Y2 are_weakly_separated & 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 SubSpace of X st
( Y1,Y2 are_weakly_separated & 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 SubSpace of X st
( Y1,Y2 are_weakly_separated & X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) )
then consider Y1, Y2 being non empty open SubSpace of X such that
A1: ( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ) by Th77;
take Y1 ; :: thesis: ex Y2 being non empty SubSpace of X st
( Y1,Y2 are_weakly_separated & X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) )
take Y2 ; :: thesis: ( Y1,Y2 are_weakly_separated & X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) )
thus ( Y1,Y2 are_weakly_separated & X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ) by A1, Th81; :: thesis: verum

end;

given Y1, Y2 being non empty SubSpace of X such that A2: Y1,Y2 are_weakly_separated and
A3: ( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 ) and
A4: ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ; :: thesis: X1,X2 are_separated
reconsider C2 = the carrier of Y2 as Subset of X by Th1;
reconsider C1 = the carrier of Y1 as Subset of X by Th1;

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 A5: ( A1 = the carrier of X1 & A2 = the carrier of X2 ) ; :: thesis: A1,A2 are_separated

now :: thesis: A1,A2 are_separated

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

suppose Y1 misses Y2 ; :: thesis: A1,A2 are_separated

then Y1,Y2 are_separated by A2, Th78;
then A6: C1,C2 are_separated ;
( A1 c= C1 & A2 c= C2 ) by A3, A5, Th4;
hence A1,A2 are_separated by A6, CONNSP_1:7; :: thesis: verum

end;

suppose A7: not Y1 misses Y2 ; :: thesis: A1,A2 are_separated

ex B1, B2 being Subset of X st
( B1,B2 are_weakly_separated & A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2 )

proof

take C1 ; :: thesis: ex B2 being Subset of X st
( C1,B2 are_weakly_separated & A1 c= C1 & A2 c= B2 & C1 /\ B2 misses A1 \/ A2 )
take C2 ; :: thesis: ( C1,C2 are_weakly_separated & A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 )
( the carrier of (Y1 meet Y2) = C1 /\ C2 & the carrier of (X1 union X2) = A1 \/ A2 ) by A5, A7, Def2, Def4;
hence ( C1,C2 are_weakly_separated & A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 ) by A2, A3, A4, A5, A7, Th4; :: thesis: verum

end;

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

end;

end;

end;

hence A1,A2 are_separated ; :: thesis: verum

end;

hence X1,X2 are_separated ; :: thesis: verum