let X be TopSpace; :: thesis:
let A1, A2 be Subset of X; :: thesis:
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:

assume A1,A2 are_separated ; :: thesis:
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 Th42;
take C1 ; :: thesis:
take C2 ; :: thesis:
( 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:

end;

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

take C1 ; :: thesis:
take C2 ; :: thesis:

end;

end;

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

end;