let M be MidSp; :: thesis: for W being ATLAS of M

for a, b1, b2, c being Point of M holds

( a @ c = b1 @ b2 iff W . (a,c) = (W . (a,b1)) + (W . (a,b2)) )

let W be ATLAS of M; :: thesis: for a, b1, b2, c being Point of M holds

( a @ c = b1 @ b2 iff W . (a,c) = (W . (a,b1)) + (W . (a,b2)) )

let a, b1, b2, c be Point of M; :: thesis: ( a @ c = b1 @ b2 iff W . (a,c) = (W . (a,b1)) + (W . (a,b2)) )

set w = the function of W;

set G = the algebra of W;

A1: ( the algebra of W is midpoint_operator & the algebra of W is add-associative & the algebra of W is right_zeroed & the algebra of W is right_complementable & the algebra of W is Abelian ) by Def12;

( the function of W is_atlas_of the carrier of M, the algebra of W & the function of W is associating ) by Def12;

hence ( a @ c = b1 @ b2 iff W . (a,c) = (W . (a,b1)) + (W . (a,b2)) ) by A1, Th27; :: thesis: verum

for a, b1, b2, c being Point of M holds

( a @ c = b1 @ b2 iff W . (a,c) = (W . (a,b1)) + (W . (a,b2)) )

let W be ATLAS of M; :: thesis: for a, b1, b2, c being Point of M holds

( a @ c = b1 @ b2 iff W . (a,c) = (W . (a,b1)) + (W . (a,b2)) )

let a, b1, b2, c be Point of M; :: thesis: ( a @ c = b1 @ b2 iff W . (a,c) = (W . (a,b1)) + (W . (a,b2)) )

set w = the function of W;

set G = the algebra of W;

A1: ( the algebra of W is midpoint_operator & the algebra of W is add-associative & the algebra of W is right_zeroed & the algebra of W is right_complementable & the algebra of W is Abelian ) by Def12;

( the function of W is_atlas_of the carrier of M, the algebra of W & the function of W is associating ) by Def12;

hence ( a @ c = b1 @ b2 iff W . (a,c) = (W . (a,b1)) + (W . (a,b2)) ) by A1, Th27; :: thesis: verum