let X, Y be set ; :: thesis: for R being Relation st X misses Y holds
( dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:]) & dom ((R ~ ) /\ [:X,Y:]) misses rng ((R ~ ) /\ [:X,Y:]) )
let R be Relation; :: thesis: ( X misses Y implies ( dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:]) & dom ((R ~ ) /\ [:X,Y:]) misses rng ((R ~ ) /\ [:X,Y:]) ) )
assume A1: X /\ Y = {} ; :: according to XBOOLE_0:def 7 :: thesis: ( dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:]) & dom ((R ~ ) /\ [:X,Y:]) misses rng ((R ~ ) /\ [:X,Y:]) )
dom (R /\ [:X,Y:]) c= X by Th13;
then A2: (dom (R /\ [:X,Y:])) /\ (rng (R /\ [:X,Y:])) c= X /\ (rng (R /\ [:X,Y:])) by XBOOLE_1:26;
X /\ (rng (R /\ [:X,Y:])) c= X /\ Y by Th13, XBOOLE_1:26;
hence (dom (R /\ [:X,Y:])) /\ (rng (R /\ [:X,Y:])) = {} by A1, A2, XBOOLE_1:1, XBOOLE_1:3; :: according to XBOOLE_0:def 7 :: thesis: dom ((R ~ ) /\ [:X,Y:]) misses rng ((R ~ ) /\ [:X,Y:])
dom ((R ~ ) /\ [:X,Y:]) c= X by Th13;
then A3: (dom ((R ~ ) /\ [:X,Y:])) /\ (rng ((R ~ ) /\ [:X,Y:])) c= X /\ (rng ((R ~ ) /\ [:X,Y:])) by XBOOLE_1:26;
X /\ (rng ((R ~ ) /\ [:X,Y:])) c= X /\ Y by Th13, XBOOLE_1:26;
hence (dom ((R ~ ) /\ [:X,Y:])) /\ (rng ((R ~ ) /\ [:X,Y:])) = {} by A1, A3, XBOOLE_1:1, XBOOLE_1:3; :: according to XBOOLE_0:def 7 :: thesis: verum