let G be Group; :: thesis: for H1, H2 being Subgroup of G holds
( H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2 )
let H1, H2 be Subgroup of G; :: thesis: ( H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2 )
H1 "\/" H2 = H2 "\/" H1 ;
hence ( H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2 ) by Lm4; :: thesis: verum