let M be MidSp; for W being ATLAS of M
for a, b, c being Point of M holds
( a @ c = b iff W . (a,c) = Double (W . (a,b)) )
let W be ATLAS of M; for a, b, c being Point of M holds
( a @ c = b iff W . (a,c) = Double (W . (a,b)) )
let a, b, c be Point of M; ( a @ c = b iff W . (a,c) = Double (W . (a,b)) )
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 = b iff W . (a,c) = Double (W . (a,b)) )
by A1, Th28; verum