let m, n be non zero Nat; :: thesis: ( m <= n implies LP<=6n+1 m <= LP<=6n+1 n )
assume m <= n ; :: thesis: LP<=6n+1 m <= LP<=6n+1 n
then <=6n+1 m c= <=6n+1 n by Th9;
hence LP<=6n+1 m <= LP<=6n+1 n by XXREAL_2:59, XBOOLE_1:26; :: thesis: verum