theorem :: GROUP_1A:139

for G being addGroup
for H1, H2 being Subgroup of G st ( H1 is finite or H2 is finite ) holds
H1 /\ H2 is finite