let G be Group; :: 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

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