set S1 = F1();
set S2 = F2();
A5: the carrier of F1() = the carrier of F2()
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the carrier of F2() c= the carrier of F1()
let x be object ; :: thesis: ( x in the carrier of F1() implies x in the carrier of F2() )
assume x in the carrier of F1() ; :: thesis: x in the carrier of F2()
then reconsider y = x as Element of F1() ;
P1[y] by A1;
then x is Element of F2() by A2;
hence x in the carrier of F2() ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of F2() or x in the carrier of F1() )
assume x in the carrier of F2() ; :: thesis: x in the carrier of F1()
then reconsider y = x as Element of F2() ;
P1[y] by A2;
then x is Element of F1() by A1;
hence x in the carrier of F1() ; :: thesis: verum
end;
the InternalRel of F1() = the InternalRel of F2()
proof
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in the InternalRel of F1() or [x,y] in the InternalRel of F2() ) & ( not [x,y] in the InternalRel of F2() or [x,y] in the InternalRel of F1() ) )
hereby :: thesis: ( not [x,y] in the InternalRel of F2() or [x,y] in the InternalRel of F1() )
assume A6: [x,y] in the InternalRel of F1() ; :: thesis: [x,y] in the InternalRel of F2()
then reconsider x1 = x, y1 = y as Element of F1() by ZFMISC_1:87;
reconsider x2 = x1, y2 = y1 as Element of F2() by A5;
x1 <= y1 by A6;
then P2[x1,y1] by A3;
then x2 <= y2 by A4;
hence [x,y] in the InternalRel of F2() ; :: thesis: verum
end;
assume A7: [x,y] in the InternalRel of F2() ; :: thesis: [x,y] in the InternalRel of F1()
then reconsider x2 = x, y2 = y as Element of F2() by ZFMISC_1:87;
reconsider x1 = x2, y1 = y2 as Element of F1() by A5;
x2 <= y2 by A7;
then P2[x2,y2] by A4;
then x1 <= y1 by A3;
hence [x,y] in the InternalRel of F1() ; :: thesis: verum
end;
hence RelStr(# the carrier of F1(), the InternalRel of F1() #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) by A5; :: thesis: verum