set S1 = F1();
set S2 = F2();
A5:
the carrier of F1() = the carrier of F2()
the InternalRel of F1() = the InternalRel of F2()
proof
let x,
y be
object ;
RELAT_1:def 2 ( ( 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() ) )
assume A7:
[x,y] in the
InternalRel of
F2()
;
[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()
;
verum
end;
hence
RelStr(# the carrier of F1(), the InternalRel of F1() #) = RelStr(# the carrier of F2(), the InternalRel of F2() #)
by A5; verum