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