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 /\ C2 misses A1 \/ A2 & 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 /\ C2 misses A1 \/ A2 & 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 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed ) ) :: thesis: ( ex C1, C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed ) implies A1,A2 are_separated )

proof

assume A1,A2 are_separated ; :: thesis: ex C1, C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed )
then consider C1, C2 being Subset of X such that
A1: ( A1 c= C1 & A2 c= C2 ) and
A2: ( C1 misses A2 & C2 misses A1 ) and
A3: ( C1 is closed & C2 is closed ) by Th46;
take C1 ; :: thesis: ex C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed )
take C2 ; :: thesis: ( A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed )
( C1 /\ C2 misses A1 & C1 /\ C2 misses A2 ) by A2, XBOOLE_1:17, XBOOLE_1:63;
hence ( A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed ) by A1, A3, XBOOLE_1:70; :: thesis: verum

end;

given C1, C2 being Subset of X such that A4: ( A1 c= C1 & A2 c= C2 ) and
A5: C1 /\ C2 misses A1 \/ A2 and
A6: ( C1 is closed & C2 is closed ) ; :: thesis: A1,A2 are_separated
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 )

proof

take C1 ; :: thesis: ex 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 C2 ; :: thesis: ( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed )

A7: now

assume C1 meets A2 ; :: thesis: contradiction
then A8: C1 /\ A2 <> {} by XBOOLE_0:def 7;
( C1 /\ A2 c= C1 /\ C2 & C1 /\ A2 c= A2 & A2 c= A1 \/ A2 ) by A4, XBOOLE_1:7, XBOOLE_1:17, XBOOLE_1:26;
then ( C1 /\ A2 c= (C1 /\ C2) /\ A2 & (C1 /\ C2) /\ A2 c= (C1 /\ C2) /\ (A1 \/ A2) ) by XBOOLE_1:19, XBOOLE_1:26;
then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A8, XBOOLE_1:1, XBOOLE_1:3;
hence contradiction by A5, XBOOLE_0:def 7; :: thesis: verum

end;

now

assume C2 meets A1 ; :: thesis: contradiction
then A9: A1 /\ C2 <> {} by XBOOLE_0:def 7;
( A1 /\ C2 c= C1 /\ C2 & A1 /\ C2 c= A1 & A1 c= A1 \/ A2 ) by A4, XBOOLE_1:7, XBOOLE_1:17, XBOOLE_1:26;
then ( A1 /\ C2 c= (C1 /\ C2) /\ A1 & (C1 /\ C2) /\ A1 c= (C1 /\ C2) /\ (A1 \/ A2) ) by XBOOLE_1:19, XBOOLE_1:26;
then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A9, XBOOLE_1:1, XBOOLE_1:3;
hence contradiction by A5, XBOOLE_0:def 7; :: thesis: verum

end;

hence ( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed ) by A4, A6, A7; :: thesis: verum

end;

hence A1,A2 are_separated by Th46; :: thesis: verum