let k be natural Number ; :: thesis: ( k > 1 implies 1 mod k = 1 )
assume A1: k > 1 ; :: thesis: 1 mod k = 1
1 = (k * 0) + 1 ;
hence 1 mod k = 1 by A1, Def2; :: thesis: verum