let x1, x2 be Element of Class F_{2}(); :: thesis: P_{1}[x1,x2]

A2: ex y2 being object st

( y2 in F_{1}() & x2 = Class (F_{2}(),y2) )
by EQREL_1:def 3;

ex y1 being object st

( y1 in F_{1}() & x1 = Class (F_{2}(),y1) )
by EQREL_1:def 3;

hence P_{1}[x1,x2]
by A1, A2; :: thesis: verum

A2: ex y2 being object st

( y2 in F

ex y1 being object st

( y1 in F

hence P