Union of two subgroups

Victor Makarov <[email protected]> Mon, 16 Nov 2020 22:34:25 -0500
Newsgroups gmane.comp.mathematics.mizar
Message-ID <CAHZyMicD_8CkOgvRJGEqs-Uo2J7LRdLGZL9XSTKmqvo3A8wLTA@mail.gmail.com>
Dear All:

I cannot find in MML a theorem that the union of two subgroups is  a
subgroup iff  one of the subgroups is a subset of the other subgroup.

The same question about the product of two subgroups H and K:

H*K is a subgroup iff H*K = K*H.

Please help.

Victor Makarov