let X be non empty TopSpace; :: thesis: for X1, X2 being closed SubSpace of X holds X1,X2 are_weakly_separated
let X1, X2 be closed 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 closed & B2 is closed ) by Th11;
hence A1,A2 are_weakly_separated by Th48; :: thesis: verum