A3: for x being set holds
( x is Element of F₃() iff P₁[x] ) by A2;
defpred S₁[ set , set ] means [$1,$2] in the InternalRel of F₁();

A4: now

let a, b be Element of F₂(); :: thesis: ( a <= b iff S₁[a,b] )
reconsider x = a, y = b as Element of F₁() by YELLOW_0:58;
( x <= y iff [x,y] in the InternalRel of F₁() ) by ORDERS_2:def 5;
hence ( a <= b iff S₁[a,b] ) by YELLOW_0:59, YELLOW_0:60; :: thesis: verum

end;

A5: now

let a, b be Element of F₃(); :: thesis: ( a <= b iff S₁[a,b] )
reconsider x = a, y = b as Element of F₁() by YELLOW_0:58;
( x <= y iff [x,y] in the InternalRel of F₁() ) by ORDERS_2:def 5;
hence ( a <= b iff S₁[a,b] ) by YELLOW_0:59, YELLOW_0:60; :: thesis: verum

end;

A6: for x being set holds
( x is Element of F₂() iff P₁[x] ) by A1;
thus RelStr(# the carrier of F₂(), the InternalRel of F₂() #) = RelStr(# the carrier of F₃(), the InternalRel of F₃() #) from WAYBEL10:sch 2(A6, A3, A4, A5); :: thesis: verum