let x be RelStr ; :: according to WAYBEL_3:def 8 :: thesis: ( not x in proj2 (MSSet (P,Q)) or x is reflexive )
assume x in rng (MSSet (P,Q)) ; :: thesis: x is reflexive
then x in {P,Q} by FUNCT_4:64;
hence x is reflexive by TARSKI:def 2; :: thesis: verum