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:24
.= (A ` ) /\ (((A ` ) ^b ) /\ ((A ^b ) /\ B)) by XBOOLE_1:16
.= (A ` ) /\ (((A ` ) ^b ) /\ {} ) by A1, XBOOLE_0:def 7
.= {} ; :: according to XBOOLE_0:def 7 :: thesis: verum