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

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