let y be Element of F₁(); :: according to RELSET_1:def 2 :: thesis: for y being Element of F₂() holds
( [y,y] in F₃() iff [y,y] in F₄() )
let z be Element of F₂(); :: thesis: ( [y,z] in F₃() iff [y,z] in F₄() )
( [y,z] in F₃() iff P₁[y,z] ) by A1;
hence ( [y,z] in F₃() iff [y,z] in F₄() ) by A2; :: thesis: verum