scheme :: WAYBEL10:sch 2
RelstrEq{ F₁() -> non empty RelStr , F₂() -> non empty RelStr , P₁[ object ], P₂[ set , set ] } :

RelStr(# the carrier of F₁(), the InternalRel of F₁() #) = RelStr(# the carrier of F₂(), the InternalRel of F₂() #)

provided

A1: for x being object holds
( x is Element of F₁() iff P₁[x] ) and
A2: for x being object holds
( x is Element of F₂() iff P₁[x] ) and
A3: for a, b being Element of F₁() holds
( a <= b iff P₂[a,b] ) and
A4: for a, b being Element of F₂() holds
( a <= b iff P₂[a,b] )