let s1, s2 be Element of NAT ; :: thesis: not ( ( x in dyadic 0 implies s1 = 0 ) & ( s1 = 0 implies x in dyadic 0 ) & ( for n being Element of 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 Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds
s2 = n + 1 ) & not s1 = s2 )
assume that
A7: ( ( x in dyadic 0 implies s1 = 0 ) & ( s1 = 0 implies x in dyadic 0 ) & ( for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds
s1 = n + 1 ) ) and
A8: ( ( x in dyadic 0 implies s2 = 0 ) & ( s2 = 0 implies x in dyadic 0 ) & ( for n being Element of 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 A7, A8; :: thesis: verum

end;

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

defpred S₁[ Nat] means x in dyadic $1;
ex s being Element of NAT st S₁[s] by A1, URYSOHN1:def 4;
then A10: 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(A10);
then consider q being Nat such that
A11: ( x in dyadic q & ( for i being Nat st x in dyadic i holds
q <= i ) ) ;

now

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

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

hence s1 = s2 by A7, A9, A11; :: thesis: verum

end;

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

then consider m being Nat such that
A12: q = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
not x in dyadic m

proof

assume x in dyadic m ; :: thesis: contradiction
then m + 1 <= m + 0 by A11, A12;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

then ( s1 = m + 1 & s2 = m + 1 ) by A7, A8, A11, A12;
hence s1 = s2 ; :: thesis: verum

end;

end;

end;

hence s1 = s2 ; :: thesis: verum

end;

end;