let G be Group; :: thesis: for H1, H2 being strict Subgroup of G holds
( H1 "\/" H2 = H2 iff H1 /\ H2 = H1 )
let H1, H2 be strict Subgroup of G; :: thesis: ( H1 "\/" H2 = H2 iff H1 /\ H2 = H1 )
( ( H1 "\/" H2 = H2 implies H1 is Subgroup of H2 ) & ( H1 is Subgroup of H2 implies H1 "\/" H2 = H2 ) & ( H1 /\ H2 = H1 implies H1 is Subgroup of H2 ) & ( H1 is Subgroup of H2 implies H1 /\ H2 = H1 ) ) by Th79, GROUP_2:107;
hence ( H1 "\/" H2 = H2 iff H1 /\ H2 = H1 ) ; :: thesis: verum