let P, R be Relation; :: thesis: ( P misses R implies P ~ misses R ~ )
assume P misses R ; :: thesis: P ~ misses R ~
then P /\ R = {} by XBOOLE_0:def 7;
then A1: (P /\ R) ~ = {} ;
(P /\ R) ~ = (P ~) /\ (R ~) by RELAT_1:22;
hence P ~ misses R ~ by XBOOLE_0:def 7, A1; :: thesis: verum