A3:
for x being object holds
( x is Element of F3() iff P1[x] )
by A2;
defpred S1[ set , set ] means [$1,$2] in the InternalRel of F1();
A4:
now for a, b being Element of F2() holds
( a <= b iff S1[a,b] )end;
A5:
now for a, b being Element of F3() holds
( a <= b iff S1[a,b] )end;
A6:
for x being object holds
( x is Element of F2() iff P1[x] )
by A1;
thus
RelStr(# the carrier of F2(), the InternalRel of F2() #) = RelStr(# the carrier of F3(), the InternalRel of F3() #)
from WAYBEL10:sch 2(A6, A3, A4, A5); verum