thus Sum (digits (198,10)) = 18 by Th88; :: according to NUMBER11:def 1 :: thesis: ( 18 divides 198 & ( for m being Nat st Sum (digits (m,10)) = 18 & 18 divides m holds
198 <= m ) )
198 = 11 * 18 ;
hence 18 divides 198 by INT_1:def 3; :: thesis: for m being Nat st Sum (digits (m,10)) = 18 & 18 divides m holds
198 <= m
let m be Nat; :: thesis: ( Sum (digits (m,10)) = 18 & 18 divides m implies 198 <= m )
assume A1: ( Sum (digits (m,10)) = 18 & 18 divides m ) ; :: thesis: 198 <= m
then consider j being Nat such that
A2: m = 18 * j by NAT_D:def 3;
assume m < 198 ; :: thesis: contradiction
then 18 * j < 18 * 11 by A2;
then j < 10 + 1 by XREAL_1:64;
then j <= 10 by NAT_1:9;
then not not j = 0 & ... & not j = 10 ;

per cases then ( j = 0 or j = 1 or j = 2 or j = 3 or j = 4 or j = 5 or j = 6 or j = 7 or j = 8 or j = 9 or j = 10 ) ;

suppose j = 0 ; :: thesis: contradiction

then Sum (digits (m,10)) = 0 by A2, Th6;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 1 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th269;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 2 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th97;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 3 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th271;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 4 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th273;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 5 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th33;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 6 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th275;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 7 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th151;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 8 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th189;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 9 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th277;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 10 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th51;
hence contradiction by A1; :: thesis: verum

end;

end;