scheme :: RELSET_1:sch 4
Sch4{ F₁() -> set , F₂() -> set , P₁[ set , set ], F₃() -> Relation of F₁(),F₂(), F₄() -> Relation of F₁(),F₂() } :

F₃() = F₄()

provided

A1: for p being Element of F₁()
for q being Element of F₂() holds
( [p,q] in F₃() iff P₁[p,q] ) and
A2: for p being Element of F₁()
for q being Element of F₂() holds
( [p,q] in F₄() iff P₁[p,q] )