let FT be non empty RelStr ; :: thesis: for A, B being Subset of FT st A,B are_separated holds
A ^deltao misses B
let A, B be Subset of FT; :: thesis: ( A,B are_separated implies A ^deltao misses B )
assume A,B are_separated ; :: thesis: A ^deltao misses B
then A1: A ^b misses B by FINTOPO4:def 1;
thus (A ^deltao) /\ B = (A `) /\ ((A ^delta) /\ B) by XBOOLE_1:16
.= (A `) /\ (((A ^b) /\ ((A `) ^b)) /\ B) by FIN_TOPO:18
.= (A `) /\ (((A `) ^b) /\ ((A ^b) /\ B)) by XBOOLE_1:16
.= (A `) /\ (((A `) ^b) /\ {}) by A1
.= {} ; :: according to XBOOLE_0:def 7 :: thesis: verum