consider G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr , w being Function of [: the carrier of M, the carrier of M:], the carrier of G such that
A1: ( w is_atlas_of the carrier of M,G & w is associating ) by Th26;
take AtlasStr(# G,w #) ; :: thesis: AtlasStr(# G,w #) is ATLAS-like
thus AtlasStr(# G,w #) is ATLAS-like by A1; :: thesis: verum