let X be non empty TopSpace; :: thesis: for X1, X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1,X2 are_weakly_separated
let X1, X2 be non empty SubSpace of X; :: thesis: ( X1 is SubSpace of X2 implies X1,X2 are_weakly_separated )

A1: now

assume A2: X1 is SubSpace of X2 ; :: thesis: ( X1 is SubSpace of X2 implies X1,X2 are_weakly_separated )

now

let A1, A2 be Subset of X; :: thesis: ( A1 = the carrier of X1 & A2 = the carrier of X2 implies A1,A2 are_weakly_separated )
assume ( A1 = the carrier of X1 & A2 = the carrier of X2 ) ; :: thesis: A1,A2 are_weakly_separated
then A1 c= A2 by A2, Th4;
hence A1,A2 are_weakly_separated by Th52; :: thesis: verum

end;

hence ( X1 is SubSpace of X2 implies X1,X2 are_weakly_separated ) by Def9; :: thesis: verum

end;

assume X1 is SubSpace of X2 ; :: thesis: X1,X2 are_weakly_separated
hence X1,X2 are_weakly_separated by A1; :: thesis: verum