defpred S1[ Nat] means x in dyadic \$1;
ex s being Nat st S1[s] by ;
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 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 end;
q <= n + 1 by A4, A5;
hence q = n + 1 by ; :: 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