let N be Element of 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 by NAT_1:7;
hence (6 * N) - 4 > 0 by A1, NAT_1:3; :: thesis: verum