set c = the carrier of F₁();
set r = the InternalRel of F₁();
set Z = { x where x is Element of the carrier of F₁() : P₁[x] } ;

now :: thesis: for x being Element of the carrier of F₁() st the InternalRel of F₁() -Seg x c= { x where x is Element of the carrier of F₁() : P₁[x] } holds
x in { x where x is Element of the carrier of F₁() : P₁[x] }

let x be Element of the carrier of F₁(); :: thesis: ( the InternalRel of F₁() -Seg x c= { x where x is Element of the carrier of F₁() : P₁[x] } implies x in { x where x is Element of the carrier of F₁() : P₁[x] } )
assume A3: the InternalRel of F₁() -Seg x c= { x where x is Element of the carrier of F₁() : P₁[x] } ; :: thesis: x in { x where x is Element of the carrier of F₁() : P₁[x] }
reconsider x9 = x as Element of F₁() ;

now :: thesis: for y9 being Element of F₁() st y9 <> x9 & [y9,x9] in the InternalRel of F₁() holds
P₁[y9]

let y9 be Element of F₁(); :: thesis: ( y9 <> x9 & [y9,x9] in the InternalRel of F₁() implies P₁[y9] )
assume ( y9 <> x9 & [y9,x9] in the InternalRel of F₁() ) ; :: thesis: P₁[y9]
then y9 in the InternalRel of F₁() -Seg x9 by WELLORD1:1;
then y9 in { x where x is Element of the carrier of F₁() : P₁[x] } by A3;
then ex y being Element of the carrier of F₁() st
( y = y9 & P₁[y] ) ;
hence P₁[y9] ; :: thesis: verum

end;

then P₁[x9] by A1;
hence x in { x where x is Element of the carrier of F₁() : P₁[x] } ; :: thesis: verum

end;

then A4: the carrier of F₁() c= { x where x is Element of the carrier of F₁() : P₁[x] } by A2, Th10;
let x be Element of F₁(); :: thesis: P₁[x]
x in { x where x is Element of the carrier of F₁() : P₁[x] } by A4;
then ex x9 being Element of the carrier of F₁() st
( x = x9 & P₁[x9] ) ;
hence P₁[x] ; :: thesis: verum