let X be TopSpace; 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 open & C2 is open ) )
let A1, A2 be Subset of X; ( 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 open & C2 is open ) )
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 ) )
( 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 ) implies A1,A2 are_separated )
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 )
; 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 )
hence
A1,A2 are_separated
by Th42; verum