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 & M,G are_associated_wrp w 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 & M,G are_associated_wrp w 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 & M,G are_associated_wrp w implies M is MidSp )
assume that
A1: w is_atlas_of the carrier of M,G and
A2: M,G are_associated_wrp w ; :: thesis: M is MidSp
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 A1, A2, Th1, Th10, Th11, Th22;
hence M is MidSp by MIDSP_1:def 4; :: thesis: verum