scheme :: FRAENKEL:sch 8
FraenkelF699{ F₁() -> set , F₂() -> set , F₃( object , object ) -> object , P₁[ object , object ], P₂[ object , object ] } :

{ F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } = { F₃(v2,u2) where u2 is Element of F₁(), v2 is Element of F₂() : P₂[u2,v2] }

provided

A1: for u being Element of F₁()
for v being Element of F₂() holds
( P₁[u,v] iff P₂[u,v] ) and
A2: for u being Element of F₁()
for v being Element of F₂() holds F₃(u,v) = F₃(v,u)