set c = the carrier of F1();
set r = the InternalRel of F1();
set Z = { x where x is Element of the carrier of F1() : P1[x] } ;
now :: thesis: for x being Element of the carrier of F1() st the InternalRel of F1() -Seg x c= { x where x is Element of the carrier of F1() : P1[x] } holds
x in { x where x is Element of the carrier of F1() : P1[x] }
let x be Element of the carrier of F1(); :: thesis: ( the InternalRel of F1() -Seg x c= { x where x is Element of the carrier of F1() : P1[x] } implies x in { x where x is Element of the carrier of F1() : P1[x] } )
assume A3: the InternalRel of F1() -Seg x c= { x where x is Element of the carrier of F1() : P1[x] } ; :: thesis: x in { x where x is Element of the carrier of F1() : P1[x] }
reconsider x9 = x as Element of F1() ;
now :: thesis: for y9 being Element of F1() st y9 <> x9 & [y9,x9] in the InternalRel of F1() holds
P1[y9]
let y9 be Element of F1(); :: thesis: ( y9 <> x9 & [y9,x9] in the InternalRel of F1() implies P1[y9] )
assume ( y9 <> x9 & [y9,x9] in the InternalRel of F1() ) ; :: thesis: P1[y9]
then y9 in the InternalRel of F1() -Seg x9 by WELLORD1:1;
then y9 in { x where x is Element of the carrier of F1() : P1[x] } by A3;
then ex y being Element of the carrier of F1() st
( y = y9 & P1[y] ) ;
hence P1[y9] ; :: thesis: verum
end;
then P1[x9] by A1;
hence x in { x where x is Element of the carrier of F1() : P1[x] } ; :: thesis: verum
end;
then A4: the carrier of F1() c= { x where x is Element of the carrier of F1() : P1[x] } by A2, Th10;
let x be Element of F1(); :: thesis: P1[x]
x in { x where x is Element of the carrier of F1() : P1[x] } by A4;
then ex x9 being Element of the carrier of F1() st
( x = x9 & P1[x9] ) ;
hence P1[x] ; :: thesis: verum