let x1, x2 be Element of Class F₂(); :: thesis: P₁[x1,x2]
A2: ex y2 being object st
( y2 in F₁() & x2 = Class (F₂(),y2) ) 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] by A1, A2; :: thesis: verum