let X be TopSpace; :: thesis: for A1, A2 being Subset of X holds
( A1,A2 are_separated iff ex C1, C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed ) )
let A1, A2 be Subset of X; :: thesis: ( A1,A2 are_separated iff ex C1, C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed ) )
thus ( A1,A2 are_separated implies ex C1, C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed ) ) :: thesis: ( ex C1, C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed ) implies A1,A2 are_separated )
proof
set C1 = Cl A1;
set C2 = Cl A2;
assume A1: A1,A2 are_separated ; :: thesis: ex C1, C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed )
take Cl A1 ; :: thesis: ex C2 being Subset of X st
( A1 c= Cl A1 & A2 c= C2 & Cl A1 misses A2 & C2 misses A1 & Cl A1 is closed & C2 is closed )
take Cl A2 ; :: thesis: ( A1 c= Cl A1 & A2 c= Cl A2 & Cl A1 misses A2 & Cl A2 misses A1 & Cl A1 is closed & Cl A2 is closed )
thus ( A1 c= Cl A1 & A2 c= Cl A2 & Cl A1 misses A2 & Cl A2 misses A1 & Cl A1 is closed & Cl A2 is closed ) by A1, CONNSP_1:def 1, PRE_TOPC:18; :: thesis: verum
end;
given C1, C2 being Subset of X such that A2: ( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed ) ; :: thesis: A1,A2 are_separated
( Cl A1 misses A2 & A1 misses Cl A2 ) by A2, TOPS_1:5, XBOOLE_1:63;
hence A1,A2 are_separated by CONNSP_1:def 1; :: thesis: verum