let X be TopSpace; :: thesis: for A1, A2 being Subset of X st A1 is closed & A2 is closed holds
( A1 misses A2 iff A1,A2 are_separated )
let A1, A2 be Subset of X; :: thesis: ( A1 is closed & A2 is closed implies ( A1 misses A2 iff A1,A2 are_separated ) )
assume A1: ( A1 is closed & A2 is closed ) ; :: thesis: ( A1 misses A2 iff A1,A2 are_separated )
thus ( A1 misses A2 implies A1,A2 are_separated ) :: thesis: ( A1,A2 are_separated implies A1 misses A2 )
proof
assume A2: A1 misses A2 ; :: thesis: A1,A2 are_separated
( Cl A1 = A1 & Cl A2 = A2 ) by A1, PRE_TOPC:22;
hence A1,A2 are_separated by A2, CONNSP_1:def 1; :: thesis: verum
end;
thus ( A1,A2 are_separated implies A1 misses A2 ) by CONNSP_1:1; :: thesis: verum