set S1 = F_{1}();

set S2 = F_{2}();

A5: the carrier of F_{1}() = the carrier of F_{2}()
_{1}() = the InternalRel of F_{2}()
_{1}(), the InternalRel of F_{1}() #) = RelStr(# the carrier of F_{2}(), the InternalRel of F_{2}() #)
by A5; :: thesis: verum

set S2 = F

A5: the carrier of F

proof
_{2}() or x in the carrier of F_{1}() )

assume x in the carrier of F_{2}()
; :: thesis: x in the carrier of F_{1}()

then reconsider y = x as Element of F_{2}() ;

P_{1}[y]
by A2;

then x is Element of F_{1}()
by A1;

hence x in the carrier of F_{1}()
; :: thesis: verum

end;

the InternalRel of Fhereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the carrier of F_{2}() c= the carrier of F_{1}()

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of Flet x be object ; :: thesis: ( x in the carrier of F_{1}() implies x in the carrier of F_{2}() )

assume x in the carrier of F_{1}()
; :: thesis: x in the carrier of F_{2}()

then reconsider y = x as Element of F_{1}() ;

P_{1}[y]
by A1;

then x is Element of F_{2}()
by A2;

hence x in the carrier of F_{2}()
; :: thesis: verum

end;assume x in the carrier of F

then reconsider y = x as Element of F

P

then x is Element of F

hence x in the carrier of F

assume x in the carrier of F

then reconsider y = x as Element of F

P

then x is Element of F

hence x in the carrier of F

proof

hence
RelStr(# the carrier of F
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in the InternalRel of F_{1}() or [x,y] in the InternalRel of F_{2}() ) & ( not [x,y] in the InternalRel of F_{2}() or [x,y] in the InternalRel of F_{1}() ) )

_{2}()
; :: thesis: [x,y] in the InternalRel of F_{1}()

then reconsider x2 = x, y2 = y as Element of F_{2}() by ZFMISC_1:87;

reconsider x1 = x2, y1 = y2 as Element of F_{1}() by A5;

x2 <= y2 by A7;

then P_{2}[x2,y2]
by A4;

then x1 <= y1 by A3;

hence [x,y] in the InternalRel of F_{1}()
; :: thesis: verum

end;hereby :: thesis: ( not [x,y] in the InternalRel of F_{2}() or [x,y] in the InternalRel of F_{1}() )

assume A7:
[x,y] in the InternalRel of Fassume A6:
[x,y] in the InternalRel of F_{1}()
; :: thesis: [x,y] in the InternalRel of F_{2}()

then reconsider x1 = x, y1 = y as Element of F_{1}() by ZFMISC_1:87;

reconsider x2 = x1, y2 = y1 as Element of F_{2}() by A5;

x1 <= y1 by A6;

then P_{2}[x1,y1]
by A3;

then x2 <= y2 by A4;

hence [x,y] in the InternalRel of F_{2}()
; :: thesis: verum

end;then reconsider x1 = x, y1 = y as Element of F

reconsider x2 = x1, y2 = y1 as Element of F

x1 <= y1 by A6;

then P

then x2 <= y2 by A4;

hence [x,y] in the InternalRel of F

then reconsider x2 = x, y2 = y as Element of F

reconsider x1 = x2, y1 = y2 as Element of F

x2 <= y2 by A7;

then P

then x1 <= y1 by A3;

hence [x,y] in the InternalRel of F