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