defpred S₁[ Nat] means x in dyadic $1;
ex s being Nat st S₁[s] by A1, URYSOHN1:def 2;
then A2: ex s being Nat st S₁[s] ;
ex q being Nat st
( S₁[q] & ( for i being Nat st S₁[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

proof

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

proof

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;

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

end;

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
q = n + 1 ) ) by A3, A4; :: thesis: verum