:: deftheorem Def28 defines PI SIN_COS:def 28 :
for b₁ being Real holds
( b₁ = PI iff ( tan . (b₁ / 4) = 1 & b₁ in ].0,4.[ ) );