let n be natural Number ; :: thesis: 0 = 0 mod n
( n = 0 or n > 0 ) ;
hence 0 = 0 mod n by Def2, Th24; :: thesis: verum