defpred S₁[ object ] means ( P₁[$1] & $1 is Element of F₁() );

A3: now :: thesis: for x being object holds
( x is Element of F₃() iff S₁[x] )

let x be object ; :: thesis: ( x is Element of F₃() iff S₁[x] )
( x is Element of F₃() implies x is Element of F₁() ) by YELLOW_0:58;
hence ( x is Element of F₃() iff S₁[x] ) by A2; :: thesis: verum

end;

A4: now :: thesis: for x being object holds
( x is Element of F₂() iff S₁[x] )

let x be object ; :: thesis: ( x is Element of F₂() iff S₁[x] )
( x is Element of F₂() implies x is Element of F₁() ) by YELLOW_0:58;
hence ( x is Element of F₂() iff S₁[x] ) by A1; :: thesis: verum

end;

thus RelStr(# the carrier of F₂(), the InternalRel of F₂() #) = RelStr(# the carrier of F₃(), the InternalRel of F₃() #) from WAYBEL10:sch 3(A4, A3); :: thesis: verum