reconsider e = 1 as odd Nat by Lm5;
take e ; :: according to NAT_6:def 5 :: thesis: ex n being positive Nat st
( 2 |^ n > e & 3 = (e * (2 |^ n)) + 1 )
take 1 ; :: thesis: ( 2 |^ 1 > e & 3 = (e * (2 |^ 1)) + 1 )
thus ( 2 |^ 1 > e & 3 = (e * (2 |^ 1)) + 1 ) ; :: thesis: verum