theorem Th12: :: NUMBER11:12

for m, n, b being Nat st b > 1 holds
( ( len (digits (m,b)) < len (digits (n,b)) or ( len (digits (m,b)) = len (digits (n,b)) & ex i being Nat st
( i < len (digits (m,b)) & (digits (m,b)) . i < (digits (n,b)) . i & ( for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j ) ) ) ) iff m < n )