defpred S_{1}[ Nat] means x in dyadic $1;

ex s being Nat st S_{1}[s]
by A1, URYSOHN1:def 2;

then A2: ex s being Nat st S_{1}[s]
;

ex q being Nat st

( S_{1}[q] & ( for i being Nat st S_{1}[i] holds

q <= i ) ) from NAT_1:sch 5(A2);

then consider q being Nat such that

A3: x in dyadic q and

A4: for i being Nat st x in dyadic i holds

q <= i ;

reconsider q = q as Nat ;

take q ; :: thesis: ( ( x in dyadic 0 implies q = 0 ) & ( q = 0 implies x in dyadic 0 ) & ( for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds

q = n + 1 ) )

for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds

q = n + 1

q = n + 1 ) ) by A3, A4; :: thesis: verum

ex s being Nat st S

then A2: ex s being Nat st S

ex q being Nat st

( S

q <= i ) ) from NAT_1:sch 5(A2);

then consider q being Nat such that

A3: x in dyadic q and

A4: for i being Nat st x in dyadic i holds

q <= i ;

reconsider q = q as Nat ;

take q ; :: thesis: ( ( x in dyadic 0 implies q = 0 ) & ( q = 0 implies x in dyadic 0 ) & ( for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds

q = n + 1 ) )

for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds

q = n + 1

proof

hence
( ( x in dyadic 0 implies q = 0 ) & ( q = 0 implies x in dyadic 0 ) & ( for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds
let n be Nat; :: thesis: ( x in dyadic (n + 1) & not x in dyadic n implies q = n + 1 )

assume that

A5: x in dyadic (n + 1) and

A6: not x in dyadic n ; :: thesis: q = n + 1

A7: n + 1 <= q

hence q = n + 1 by A7, XXREAL_0:1; :: thesis: verum

end;assume that

A5: x in dyadic (n + 1) and

A6: not x in dyadic n ; :: thesis: q = n + 1

A7: n + 1 <= q

proof

q <= n + 1
by A4, A5;
assume
not n + 1 <= q
; :: thesis: contradiction

then q <= n by NAT_1:13;

then dyadic q c= dyadic n by URYSOHN2:29;

hence contradiction by A3, A6; :: thesis: verum

end;then q <= n by NAT_1:13;

then dyadic q c= dyadic n by URYSOHN2:29;

hence contradiction by A3, A6; :: thesis: verum

hence q = n + 1 by A7, XXREAL_0:1; :: thesis: verum

q = n + 1 ) ) by A3, A4; :: thesis: verum