take 2 ; :: according to ASYMPT_0:def 4 :: thesis: for b₁ being set holds
( not 2 <= b₁ or not seq_logn . b₁ <= 0 )
set f = seq_logn ;
let n be Nat; :: thesis: ( not 2 <= n or not seq_logn . n <= 0 )
A1: n in NAT by ORDINAL1:def 12;
assume A2: n >= 2 ; :: thesis: not seq_logn . n <= 0
then A3: log (2,n) >= log (2,2) by PRE_FF:10;
seq_logn . n = log (2,n) by A2, Def2, A1;
hence not seq_logn . n <= 0 by A3, POWER:52; :: thesis: verum