let G be Group; :: thesis: for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 holds
H1 is Subgroup of H2 "\/" H3
let H1, H2, H3 be Subgroup of G; :: thesis: ( H1 is Subgroup of H2 implies H1 is Subgroup of H2 "\/" H3 )
H2 is Subgroup of H2 "\/" H3 by Th60;
hence ( H1 is Subgroup of H2 implies H1 is Subgroup of H2 "\/" H3 ) by GROUP_2:56; :: thesis: verum