begin
Lm1:
for x being set
for G being non empty 1-sorted
for A being Subset of G st x in A holds
x is Element of G
;
Lm2:
for A being commutative Group
for a, b being Element of A holds a * b = b * a
;
Lm3:
for G being Group
for H2, H1 being Subgroup of G holds
( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) )
Lm4:
for G being Group
for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1
Lm5:
for k being Nat
for X being finite set st ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) holds
ex C being finite set st
( C = union X & card C = k * (card X) )