set c = the carrier of F_{1}();

set r = the InternalRel of F_{1}();

set Z = { x where x is Element of the carrier of F_{1}() : P_{1}[x] } ;

_{1}() c= { x where x is Element of the carrier of F_{1}() : P_{1}[x] }
by A2, Th10;

let x be Element of F_{1}(); :: thesis: P_{1}[x]

x in { x where x is Element of the carrier of F_{1}() : P_{1}[x] }
by A4;

then ex x9 being Element of the carrier of F_{1}() st

( x = x9 & P_{1}[x9] )
;

hence P_{1}[x]
; :: thesis: verum

set r = the InternalRel of F

set Z = { x where x is Element of the carrier of F

now :: thesis: for x being Element of the carrier of F_{1}() st the InternalRel of F_{1}() -Seg x c= { x where x is Element of the carrier of F_{1}() : P_{1}[x] } holds

x in { x where x is Element of the carrier of F_{1}() : P_{1}[x] }

then A4:
the carrier of Fx in { x where x is Element of the carrier of F

let x be Element of the carrier of F_{1}(); :: thesis: ( the InternalRel of F_{1}() -Seg x c= { x where x is Element of the carrier of F_{1}() : P_{1}[x] } implies x in { x where x is Element of the carrier of F_{1}() : P_{1}[x] } )

assume A3: the InternalRel of F_{1}() -Seg x c= { x where x is Element of the carrier of F_{1}() : P_{1}[x] }
; :: thesis: x in { x where x is Element of the carrier of F_{1}() : P_{1}[x] }

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

_{1}[x9]
by A1;

hence x in { x where x is Element of the carrier of F_{1}() : P_{1}[x] }
; :: thesis: verum

end;assume A3: the InternalRel of F

reconsider x9 = x as Element of F

now :: thesis: for y9 being Element of F_{1}() st y9 <> x9 & [y9,x9] in the InternalRel of F_{1}() holds

P_{1}[y9]

then
PP

let y9 be Element of F_{1}(); :: thesis: ( y9 <> x9 & [y9,x9] in the InternalRel of F_{1}() implies P_{1}[y9] )

assume ( y9 <> x9 & [y9,x9] in the InternalRel of F_{1}() )
; :: thesis: P_{1}[y9]

then y9 in the InternalRel of F_{1}() -Seg x9
by WELLORD1:1;

then y9 in { x where x is Element of the carrier of F_{1}() : P_{1}[x] }
by A3;

then ex y being Element of the carrier of F_{1}() st

( y = y9 & P_{1}[y] )
;

hence P_{1}[y9]
; :: thesis: verum

end;assume ( y9 <> x9 & [y9,x9] in the InternalRel of F

then y9 in the InternalRel of F

then y9 in { x where x is Element of the carrier of F

then ex y being Element of the carrier of F

( y = y9 & P

hence P

hence x in { x where x is Element of the carrier of F

let x be Element of F

x in { x where x is Element of the carrier of F

then ex x9 being Element of the carrier of F

( x = x9 & P

hence P