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

A3: now

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

end;

A4: now

let x be set ; :: thesis: ( x is Element of F₃() iff S₁[x] )
( x is Element of F₃() implies x is Element of F₁() ) by YELLOW_0:59;
hence ( x is Element of F₃() iff S₁[x] ) by A2; :: 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(A3, A4); :: thesis: verum