take 0 ; :: according to ASYMPT_0:def 2 :: thesis: for b₁ being set holds
( not 0 <= b₁ or 0 <= (seq_const 1) . b₁ )
let n be Nat; :: thesis: ( not 0 <= n or 0 <= (seq_const 1) . n )
assume n >= 0 ; :: thesis: 0 <= (seq_const 1) . n
thus 0 <= (seq_const 1) . n ; :: thesis: verum