set A = { x where x is Element of F1() : P1[x] } ;
consider z being Element of F1() such that
A3: P1[z] by A1;
A4: z in { x where x is Element of F1() : P1[x] } by A3;
now :: thesis: for x being Element of F1() st x in { x where x is Element of F1() : P1[x] } holds
ex y being Element of F1() st
( y in { x where x is Element of F1() : P1[x] } & x ==> y )
let x be Element of F1(); :: thesis: ( x in { x where x is Element of F1() : P1[x] } implies ex y being Element of F1() st
( y in { x where x is Element of F1() : P1[x] } & x ==> y ) )

assume x in { x where x is Element of F1() : P1[x] } ; :: thesis: ex y being Element of F1() st
( y in { x where x is Element of F1() : P1[x] } & x ==> y )

then ex a being Element of F1() st
( x = a & P1[a] ) ;
then consider y being Element of F1() such that
A6: ( P1[y] & x ==> y ) by A2;
take y = y; :: thesis: ( y in { x where x is Element of F1() : P1[x] } & x ==> y )
thus y in { x where x is Element of F1() : P1[x] } by A6; :: thesis: x ==> y
thus x ==> y by A6; :: thesis: verum
end;
hence not F1() is SN by ; :: thesis: verum