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 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();
( 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] }
;
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;
( 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;
x ==> ythus
x ==> y
by A6;
verum end;
hence
not F1() is SN
by A4, ThSN; verum