let X, R be set ; :: thesis: ( not X is with_pair & R is Relation implies X misses R )
assume A1: for x being pair set holds not x in X ; :: according to FACIRC_1:def 2 :: thesis: ( not R is Relation or X misses R )
assume A2: R is Relation ; :: thesis: X misses R

now

let x be set ; :: thesis: ( x in X implies not x in R )
assume x in X ; :: thesis: not x in R
then for z1, z2 being set holds not x = [z1,z2] by A1;
hence not x in R by A2, RELAT_1:def 1; :: thesis: verum

end;

hence X misses R by XBOOLE_0:3; :: thesis: verum