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 and
A2: M,G are_associated_wrp w by Th33;
take AtlasStr(# G,w #) ; :: thesis: AtlasStr(# G,w #) is ATLAS-like
thus AtlasStr(# G,w #) is ATLAS-like by A1, A2, Def12; :: thesis: verum