let c be Integer; :: thesis: ( c > 1 implies 1 mod c = 1 )
assume A1: c > 1 ; :: thesis: 1 mod c = 1
then 1 div c = 0 by PRE_FF:4;
then 1 mod c = 1 - (0 * c) by A1, INT_1:def 10;
hence 1 mod c = 1 ; :: thesis: verum