scheme :: WAYBEL10:sch 4
SubrelstrEq2{ F₁() -> non empty RelStr , F₂() -> non empty full SubRelStr of F₁(), F₃() -> non empty full SubRelStr of F₁(), P₁[ object ] } :

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

provided

A1: for x being Element of F₁() holds
( x is Element of F₂() iff P₁[x] ) and
A2: for x being Element of F₁() holds
( x is Element of F₃() iff P₁[x] )