let X be non empty TopSpace; :: thesis: for X1, X2 being open SubSpace of X holds X1,X2 are_weakly_separated
let X1, X2 be open SubSpace of X; :: thesis: X1,X2 are_weakly_separated
let A1, A2 be Subset of X; :: according to TSEP_1:def 7 :: thesis: ( A1 = the carrier of X1 & A2 = the carrier of X2 implies A1,A2 are_weakly_separated )
reconsider B1 = A1, B2 = A2 as Subset of X ;
assume ( A1 = the carrier of X1 & A2 = the carrier of X2 ) ; :: thesis: A1,A2 are_weakly_separated
then ( B1 is open & B2 is open ) by Th16;
hence A1,A2 are_weakly_separated by Th49; :: thesis: verum