let w1, w2 be Point of (TOP-REAL n); :: according to CONVEX1:def 2 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or 1 <= b₁ or not w1 in [#] (TOP-REAL n) or not w2 in [#] (TOP-REAL n) or K258((TOP-REAL n),(b₁ * w1),((1 - b₁) * w2)) in [#] (TOP-REAL n) )
thus for b₁ being Element of REAL holds
( b₁ <= 0 or 1 <= b₁ or not w1 in [#] (TOP-REAL n) or not w2 in [#] (TOP-REAL n) or K258((TOP-REAL n),(b₁ * w1),((1 - b₁) * w2)) in [#] (TOP-REAL n) ) ; :: thesis: verum