let X be TopSpace; :: thesis: for A1, A2 being Subset of X st A1 is open & A2 is open holds
A1,A2 are_weakly_separated
let A1, A2 be Subset of X; :: thesis: ( A1 is open & A2 is open implies A1,A2 are_weakly_separated )
assume A1: ( A1 is open & A2 is open ) ; :: thesis: A1,A2 are_weakly_separated
( A2 misses A1 \ A2 & A2 \ A1 misses A1 ) by XBOOLE_1:79;
then ( A2 misses Cl (A1 \ A2) & Cl (A2 \ A1) misses A1 ) by A1, Th40;
then ( Cl (A1 \ A2) misses A2 \ A1 & A1 \ A2 misses Cl (A2 \ A1) ) by XBOOLE_1:36, XBOOLE_1:63;
then A1 \ A2,A2 \ A1 are_separated by CONNSP_1:def 1;
hence A1,A2 are_weakly_separated by Def7; :: thesis: verum