let s1, s2 be Nat; :: thesis: not ( ( x in dyadic 0 implies s1 = 0 ) & ( s1 = 0 implies x in dyadic 0 ) & ( for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds
s1 = n + 1 ) & ( x in dyadic 0 implies s2 = 0 ) & ( s2 = 0 implies x in dyadic 0 ) & ( for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds
s2 = n + 1 ) & not s1 = s2 )
assume that
A8: ( x in dyadic 0 iff s1 = 0 ) and
A9: for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds
s1 = n + 1 and
A10: ( x in dyadic 0 iff s2 = 0 ) and
A11: for n being Nat st x in dyadic (n + 1) & not x in dyadic n holds
s2 = n + 1 ; :: thesis: s1 = s2

per cases ( s1 = 0 or 0 < s1 ) ;

suppose s1 = 0 ; :: thesis: s1 = s2

hence s1 = s2 by A8, A10; :: thesis: verum

end;

suppose A12: 0 < s1 ; :: thesis: s1 = s2

defpred S₁[ Nat] means x in dyadic $1;
ex s being Nat st S₁[s] by A1, URYSOHN1:def 2;
then A13: 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(A13);
then consider q being Nat such that
A14: x in dyadic q and
A15: for i being Nat st x in dyadic i holds
q <= i ;

now :: thesis: ( ( q = 0 & s1 = s2 ) or ( 0 < q & s1 = s2 ) )

per cases ( q = 0 or 0 < q ) ;

case q = 0 ; :: thesis: s1 = s2

hence s1 = s2 by A8, A12, A14; :: thesis: verum

end;

case 0 < q ; :: thesis: s1 = s2

then consider m being Nat such that
A16: q = m + 1 by NAT_1:6;
reconsider m = m as Nat ;
A17: not x in dyadic m

proof

assume x in dyadic m ; :: thesis: contradiction
then m + 1 <= m + 0 by A15, A16;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

then s1 = m + 1 by A9, A14, A16;
hence s1 = s2 by A11, A14, A16, A17; :: thesis: verum

end;

end;

end;

hence s1 = s2 ; :: thesis: verum

end;

end;