let X be TopSpace; :: thesis: for A1, A2 being Subset of X st A1 c= A2 holds
A1,A2 are_weakly_separated
let A1, A2 be Subset of X; :: thesis: ( A1 c= A2 implies A1,A2 are_weakly_separated )
A1: now :: thesis: ( A1 c= A2 & A1 c= A2 implies A1,A2 are_weakly_separated )
assume A1 c= A2 ; :: thesis: ( A1 c= A2 implies A1,A2 are_weakly_separated )
then A2: A1 \ A2 = {} by XBOOLE_1:37;
then Cl (A1 \ A2) = {} by PRE_TOPC:22;
then (Cl (A1 \ A2)) /\ (A2 \ A1) = {} ;
then A3: Cl (A1 \ A2) misses A2 \ A1 by XBOOLE_0:def 7;
(A1 \ A2) /\ (Cl (A2 \ A1)) = {} by A2;
then A1 \ A2 misses Cl (A2 \ A1) by XBOOLE_0:def 7;
then A1 \ A2,A2 \ A1 are_separated by A3, CONNSP_1:def 1;
hence ( A1 c= A2 implies A1,A2 are_weakly_separated ) ; :: thesis: verum
end;
assume A1 c= A2 ; :: thesis: A1,A2 are_weakly_separated
hence A1,A2 are_weakly_separated by A1; :: thesis: verum