let x be set ; :: according to YELLOW_1:def 3 :: thesis: ( not x in rng (MSSet P,Q) or x is RelStr )
assume x in rng (MSSet P,Q) ; :: thesis: x is RelStr
then x in {P,Q} by FUNCT_4:67;
hence x is RelStr by TARSKI:def 2; :: thesis: verum