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

A2: ex y2 being object st

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

A3: ex y3 being object st

( y3 in F_{1}() & x3 = Class (F_{2}(),y3) )
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,x3]
by A1, A2, A3; :: thesis: verum

A2: ex y2 being object st

( y2 in F

A3: ex y3 being object st

( y3 in F

ex y1 being object st

( y1 in F

hence P