set A = { x where x is Element of F₁() : P₁[x] } ;
consider z being Element of F₁() such that
A3: P₁[z] by A1;
A4: z in { x where x is Element of F₁() : P₁[x] } by A3;

now :: thesis: for x being Element of F₁() st x in { x where x is Element of F₁() : P₁[x] } holds
ex y being Element of F₁() st
( y in { x where x is Element of F₁() : P₁[x] } & x ==> y )

let x be Element of F₁(); :: thesis: ( x in { x where x is Element of F₁() : P₁[x] } implies ex y being Element of F₁() st
( y in { x where x is Element of F₁() : P₁[x] } & x ==> y ) )
assume x in { x where x is Element of F₁() : P₁[x] } ; :: thesis: ex y being Element of F₁() st
( y in { x where x is Element of F₁() : P₁[x] } & x ==> y )
then ex a being Element of F₁() st
( x = a & P₁[a] ) ;
then consider y being Element of F₁() such that
A6: ( P₁[y] & x ==> y ) by A2;
take y = y; :: thesis: ( y in { x where x is Element of F₁() : P₁[x] } & x ==> y )
thus y in { x where x is Element of F₁() : P₁[x] } by A6; :: thesis: x ==> y
thus x ==> y by A6; :: thesis: verum

end;

hence not F₁() is SN by A4, ThSN; :: thesis: verum