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

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 )
;

end;

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

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

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

then A13: 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(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 ;

end;ex s being Nat st S

then A13: ex s being Nat st S

ex q being Nat st

( S

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 ) )end;

hence
s1 = s2
; :: thesis: verumper cases
( q = 0 or 0 < q )
;

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

hence s1 = s2 by A11, A14, A16, A17; :: thesis: verum

end;A16: q = m + 1 by NAT_1:6;

reconsider m = m as Nat ;

A17: not x in dyadic m

proof

then
s1 = m + 1
by A9, A14, A16;
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 m + 1 <= m + 0 by A15, A16;

hence contradiction by XREAL_1:6; :: thesis: verum

hence s1 = s2 by A11, A14, A16, A17; :: thesis: verum