given a being object such that A3: a in field F₁() and
A4: P₁[a] ; :: thesis: contradiction
reconsider X = field F₁() as non empty set by A3;
reconsider a = a as Element of X by A3;
set Y = { x where x is Element of X : P₁[x] } ;
A5: a in { x where x is Element of X : P₁[x] } by A4;
{ x where x is Element of X : P₁[x] } c= field F₁()

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of X : P₁[x] } or y in field F₁() )
assume y in { x where x is Element of X : P₁[x] } ; :: thesis: y in field F₁()
then ex x being Element of X st
( y = x & P₁[x] ) ;
hence y in field F₁() ; :: thesis: verum

end;

then consider a being object such that
A6: a in { x where x is Element of X : P₁[x] } and
A7: for b being object st b in { x where x is Element of X : P₁[x] } & a <> b holds
not [a,b] in F₁() by A1, A5;

A8: now :: thesis: for b being object st [a,b] in F₁() & a <> b holds
P₁[b]

let b be object ; :: thesis: ( [a,b] in F₁() & a <> b implies P₁[b] )
assume that
A9: ( [a,b] in F₁() & a <> b ) and
A10: P₁[b] ; :: thesis: contradiction
( not b in { x where x is Element of X : P₁[x] } & b in X ) by A7, A9, RELAT_1:15;
hence contradiction by A10; :: thesis: verum

end;

ex x being Element of X st
( a = x & P₁[x] ) by A6;
hence contradiction by A2, A8; :: thesis: verum