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

let x be object ; :: thesis:
( 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:

end;

let x be object ; :: thesis:
( 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:

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: