let y, z be object ; :: according to RELAT_1:def 2 :: thesis: ( [y,z] in F₁() iff [y,z] in F₂() )
thus ( [y,z] in F₁() implies [y,z] in F₂() ) by A1, A2; :: thesis: ( [y,z] in F₂() implies [y,z] in F₁() )
assume [y,z] in F₂() ; :: thesis: [y,z] in F₁()
hence [y,z] in F₁() by A1, A2; :: thesis: verum