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