let FT be non empty RelStr ; :: thesis: for A being Subset of FT holds A ^deltai misses A ^deltao
let A be Subset of FT; :: thesis: A ^deltai misses A ^deltao
A misses A ` by XBOOLE_1:79;
then A1: A /\ (A ` ) = {} by XBOOLE_0:def 7;
thus (A ^deltai ) /\ (A ^deltao ) = (A /\ ((A ^delta ) /\ (A ` ))) /\ (A ^delta ) by XBOOLE_1:16
.= ((A /\ (A ` )) /\ (A ^delta )) /\ (A ^delta ) by XBOOLE_1:16
.= {} by A1 ; :: according to XBOOLE_0:def 7 :: thesis: verum