let M be MidSp; :: thesis: for W being ATLAS of M
for a, c, b1, b2 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, c, b1, b2 being Point of M holds
( a @ c = b1 @ b2 iff W . a,c = (W . a,b1) + (W . a,b2) )
let a, c, b1, b2 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 & M,the algebra of W are_associated_wrp the function of W ) by Def12;
hence ( a @ c = b1 @ b2 iff W . a,c = (W . a,b1) + (W . a,b2) ) by A1, Th34; :: thesis: verum