set G = the strict Group;
consider H being non empty HGrWOpStr over O such that
A1: ( H is strict & H is distributive & H is Group-like & H is associative ) and
multMagma(# the carrier of H, the multF of H #) = the strict Group by Lm2;
take H ; :: thesis: ( H is strict & H is distributive & H is Group-like & H is associative )
thus ( H is strict & H is distributive & H is Group-like & H is associative ) by A1; :: thesis: verum