let g be FinSequence of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st <*p,q*> is_in_the_area_of g holds
<*((1 / 2) * (p + q))*> is_in_the_area_of g
let p, q be Point of (TOP-REAL 2); :: thesis: ( <*p,q*> is_in_the_area_of g implies <*((1 / 2) * (p + q))*> is_in_the_area_of g )
(1 / 2) * (p + q) = ((1 - (1 / 2)) * p) + ((1 / 2) * q) by EUCLID:32;
hence ( <*p,q*> is_in_the_area_of g implies <*((1 / 2) * (p + q))*> is_in_the_area_of g ) by Th61; :: thesis: verum