let k be Nat; P1[k]
consider X being Subset of NAT such that
A3:
for x being Element of NAT holds
( x in X iff P1[x] )
from SUBSET_1:sch 3();
A4:
for x being Real st x in X holds
x + 1 in X
proof
let x be
Real;
( x in X implies x + 1 in X )
assume
x in X
;
x + 1 in X
then consider k being
Nat such that A5:
P1[
k]
and A6:
k = x
by A3;
P1[
k + 1]
by A2, A5;
hence
x + 1
in X
by A3, A6;
verum
end;
( X c= NAT & NAT c= REAL )
by NUMBERS:19;
then
X is Subset of REAL
by XBOOLE_1:1;
then
k in X
by A1, A3, A4, Th1;
hence
P1[k]
by A3; verum