let x be object ; :: according to RELAT_1:def 1 :: thesis: ( x in P \/ R implies ex y, z being object st x = [y,z] )
A1: ( x in R implies ex y, z being object st x = [y,z] ) by Def1;
( x in P implies ex y, z being object st x = [y,z] ) by Def1;
hence ( x in P \/ R implies ex y, z being object st x = [y,z] ) by A1, XBOOLE_0:def 3; :: thesis: verum