:: deftheorem Def8 defines w_seq WALLIS01:def 7 :
for b₁ being Real_Sequence holds
( b₁ = w_seq iff for n being Nat holds b₁ . n = 1 / ((1 + (1 / (2 * (n + 1)))) * PI) );