let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ; :: thesis: for M being non empty MidStr

for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds

M is MidSp

let M be non empty MidStr ; :: thesis: for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds

M is MidSp

let w be Function of [: the carrier of M, the carrier of M:], the carrier of G; :: thesis: ( w is_atlas_of the carrier of M,G & w is associating implies M is MidSp )

assume ( w is_atlas_of the carrier of M,G & w is associating ) ; :: thesis: M is MidSp

then for a, b, c, d being Point of M holds

( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Point of M st x @ a = b ) by Th1, Th8, Th9, Th19;

hence M is MidSp by MIDSP_1:def 3; :: thesis: verum

for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds

M is MidSp

let M be non empty MidStr ; :: thesis: for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds

M is MidSp

let w be Function of [: the carrier of M, the carrier of M:], the carrier of G; :: thesis: ( w is_atlas_of the carrier of M,G & w is associating implies M is MidSp )

assume ( w is_atlas_of the carrier of M,G & w is associating ) ; :: thesis: M is MidSp

then for a, b, c, d being Point of M holds

( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Point of M st x @ a = b ) by Th1, Th8, Th9, Th19;

hence M is MidSp by MIDSP_1:def 3; :: thesis: verum