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 :: thesis: for a, b being Element of F2() holds
( a <= b iff S1[a,b] )
let a, b be Element of F2(); :: thesis: ( a <= b iff S1[a,b] )
reconsider x = a, y = b as Element of F1() by YELLOW_0:58;
( x <= y iff [x,y] in the InternalRel of F1() ) ;
hence ( a <= b iff S1[a,b] ) by YELLOW_0:59, YELLOW_0:60; :: thesis: verum
end;
A5: now :: thesis: for a, b being Element of F3() holds
( a <= b iff S1[a,b] )
let a, b be Element of F3(); :: thesis: ( a <= b iff S1[a,b] )
reconsider x = a, y = b as Element of F1() by YELLOW_0:58;
( x <= y iff [x,y] in the InternalRel of F1() ) ;
hence ( a <= b iff S1[a,b] ) by YELLOW_0:59, YELLOW_0:60; :: thesis: verum
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); :: thesis: verum