defpred S1[ Nat] means x indyadic $1;
ex s being Nat st S1[s]
byA1, URYSOHN1:def 2; then A13:
ex s being Nat st S1[s]
;
ex q being Nat st ( S1[q] & ( for i being Nat st S1[i] holds q <= i ) )
fromNAT_1:sch 5(A13); then consider q being Nat such that A14:
x indyadic q
and A15:
for i being Nat st x indyadic i holds q <= i
;