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