let x1, x2, x3 be Element of Class F₂(); :: thesis: P₁[x1,x2,x3]
A2: ex y2 being object st
( y2 in F₁() & x2 = Class (F₂(),y2) ) by EQREL_1:def 3;
A3: ex y3 being object st
( y3 in F₁() & x3 = Class (F₂(),y3) ) by EQREL_1:def 3;
ex y1 being object st
( y1 in F₁() & x1 = Class (F₂(),y1) ) by EQREL_1:def 3;
hence P₁[x1,x2,x3] by A1, A2, A3; :: thesis: verum