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 `) = {} ;
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