A3:
for x being object holds

( x is Element of F_{3}() iff P_{1}[x] )
by A2;

defpred S_{1}[ set , set ] means [$1,$2] in the InternalRel of F_{1}();

( x is Element of F_{2}() iff P_{1}[x] )
by A1;

thus RelStr(# the carrier of F_{2}(), the InternalRel of F_{2}() #) = RelStr(# the carrier of F_{3}(), the InternalRel of F_{3}() #)
from WAYBEL10:sch 2(A6, A3, A4, A5); :: thesis: verum

( x is Element of F

defpred S

A4: now :: thesis: for a, b being Element of F_{2}() holds

( a <= b iff S_{1}[a,b] )

( a <= b iff S

let a, b be Element of F_{2}(); :: thesis: ( a <= b iff S_{1}[a,b] )

reconsider x = a, y = b as Element of F_{1}() by YELLOW_0:58;

( x <= y iff [x,y] in the InternalRel of F_{1}() )
;

hence ( a <= b iff S_{1}[a,b] )
by YELLOW_0:59, YELLOW_0:60; :: thesis: verum

end;reconsider x = a, y = b as Element of F

( x <= y iff [x,y] in the InternalRel of F

hence ( a <= b iff S

A5: now :: thesis: for a, b being Element of F_{3}() holds

( a <= b iff S_{1}[a,b] )

A6:
for x being object holds ( a <= b iff S

let a, b be Element of F_{3}(); :: thesis: ( a <= b iff S_{1}[a,b] )

reconsider x = a, y = b as Element of F_{1}() by YELLOW_0:58;

( x <= y iff [x,y] in the InternalRel of F_{1}() )
;

hence ( a <= b iff S_{1}[a,b] )
by YELLOW_0:59, YELLOW_0:60; :: thesis: verum

end;reconsider x = a, y = b as Element of F

( x <= y iff [x,y] in the InternalRel of F

hence ( a <= b iff S

( x is Element of F

thus RelStr(# the carrier of F