let N be Nat; :: thesis: ( N <> 0 implies (6 * N) - 4 > 0 )
assume N <> 0 ; :: thesis: (6 * N) - 4 > 0
then consider L being Nat such that
A1: N = L + 1 by NAT_1:6;
reconsider L = L as Element of NAT by ORDINAL1:def 12;
(6 * L) + 2 <> 0 ;
hence (6 * N) - 4 > 0 by A1; :: thesis: verum