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 misses A2 & C2 misses A1 & C1 is open & C2 is open ) ) :: thesis:

proof

assume A1,A2 are_separated ; :: thesis:
then consider C1, C2 being Subset of X such that
A1: ( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed ) by Th42;
take C2 ` ; :: thesis:
take C1 ` ; :: thesis:
thus ( A1 c= C2 ` & A2 c= C1 ` & C2 ` misses A2 & C1 ` misses A1 & C2 ` is open & C1 ` is open ) by A1, SUBSET_1:23, SUBSET_1:24; :: thesis:

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 open & C2 is open ) ; :: 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 )

proof

take C2 ` ; :: thesis:
take C1 ` ; :: thesis:
thus ( A1 c= C2 ` & A2 c= C1 ` & C2 ` misses A2 & C1 ` misses A1 & C2 ` is closed & C1 ` is closed ) by A2, SUBSET_1:23, SUBSET_1:24; :: thesis:

end;

hence A1,A2 are_separated by Th42; :: thesis: