let X be TopSpace; 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; ( A1 is closed & A2 is closed implies A1,A2 are_weakly_separated )
assume that
A1:
A1 is closed
and
A2:
A2 is closed
; 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
; verum