let y be Element of F_{1}(); :: according to RELSET_1:def 2 :: thesis: for y being Element of F_{2}() holds

( [y,y] in F_{3}() iff [y,y] in F_{4}() )

let z be Element of F_{2}(); :: thesis: ( [y,z] in F_{3}() iff [y,z] in F_{4}() )

( [y,z] in F_{3}() iff P_{1}[y,z] )
by A1;

hence ( [y,z] in F_{3}() iff [y,z] in F_{4}() )
by A2; :: thesis: verum

( [y,y] in F

let z be Element of F

( [y,z] in F

hence ( [y,z] in F