let G be addGroup; :: thesis: for H1, H2 being Subgroup of G st ( H1 is finite or H2 is finite ) holds
H1 /\ H2 is finite
let H1, H2 be Subgroup of G; :: thesis: ( ( H1 is finite or H2 is finite ) implies H1 /\ H2 is finite )
assume A1: ( H1 is finite or H2 is finite ) ; :: thesis: H1 /\ H2 is finite
( H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2 ) by Lm4;
hence H1 /\ H2 is finite by A1; :: thesis: verum