let y, z be set ; :: according to RELAT_1:def 2 :: thesis: ( [y,z] in F₁() iff [y,z] in F₂() )

hereby :: thesis: ( [y,z] in F₂() implies [y,z] in F₁() )

assume [y,z] in F₁() ; :: thesis: [y,z] in F₂()
then P₁[y,z] by A1;
hence [y,z] in F₂() by A2; :: thesis: verum

end;

assume [y,z] in F₂() ; :: thesis: [y,z] in F₁()
then P₁[y,z] by A2;
hence [y,z] in F₁() by A1; :: thesis: verum