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 iff H1 is Subgroup of H2 ) by Th61;
hence ( H1 "\/" H2 = H2 iff H1 /\ H2 = H1 ) by GROUP_2:89; :: thesis: verum