let m be Nat; :: thesis: for t being Integer st m * t >= 1 holds
t >= 1
let t be Integer; :: thesis: ( m * t >= 1 implies t >= 1 )
assume A1: m * t >= 1 ; :: thesis: t >= 1
assume t < 1 ; :: thesis: contradiction
then t <= 0 by Lm1;
hence contradiction by A1; :: thesis: verum