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