let X be TopSpace; :: thesis: for A1, A2 being Subset of X st A1 is closed & A2 is closed holds
A1,A2 are_weakly_separated
let A1, A2 be Subset of X; :: thesis: ( A1 is closed & A2 is closed implies A1,A2 are_weakly_separated )
assume that
A1: A1 is closed and
A2: A2 is closed ; :: thesis: A1,A2 are_weakly_separated
Cl (A2 \ A1) c= A2 by A2, TOPS_1:5, XBOOLE_1:36;
then (Cl (A2 \ A1)) \ A2 = {} by XBOOLE_1:37;
then A3: A1 \ A2 misses Cl (A2 \ A1) by Lm1;
Cl (A1 \ A2) c= A1 by A1, TOPS_1:5, XBOOLE_1:36;
then (Cl (A1 \ A2)) \ A1 = {} by XBOOLE_1:37;
then Cl (A1 \ A2) misses A2 \ A1 by Lm1;
then A1 \ A2,A2 \ A1 are_separated by A3, CONNSP_1:def 1;
hence A1,A2 are_weakly_separated ; :: thesis: verum