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

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 x' = x as Element of ;

now

let y' be Element of ; :: thesis: ( y' <> x' & [y',x'] in the InternalRel of F₁() implies P₁[y'] )
assume ( y' <> x' & [y',x'] in the InternalRel of F₁() ) ; :: thesis: P₁[y']
then y' in the InternalRel of F₁() -Seg x' by WELLORD1:def 1;
then y' 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 = y' & P₁[y] ) ;
hence P₁[y'] ; :: thesis: verum

end;

then P₁[x'] 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, Th11;
let x be Element of ; :: thesis: P₁[x]
x in the carrier of F₁() ;
then x in { x where x is Element of the carrier of F₁() : P₁[x] } by A4;
then ex x' being Element of the carrier of F₁() st
( x = x' & P₁[x'] ) ;
hence P₁[x] ; :: thesis: verum