theorem Th509: :: NUMBER11:509

Sum (digits (1800,10)) = 9