let G be Group; :: thesis: for H1 being Subgroup of G
for H2 being strict Subgroup of G holds
( H1 is Subgroup of H2 iff H1 "\/" H2 = H2 )
let H1 be Subgroup of G; :: thesis: for H2 being strict Subgroup of G holds
( H1 is Subgroup of H2 iff H1 "\/" H2 = H2 )
let H2 be strict Subgroup of G; :: thesis: ( H1 is Subgroup of H2 iff H1 "\/" H2 = H2 )
thus ( H1 is Subgroup of H2 implies H1 "\/" H2 = H2 ) :: thesis: ( H1 "\/" H2 = H2 implies H1 is Subgroup of H2 )

proof

assume H1 is Subgroup of H2 ; :: thesis: H1 "\/" H2 = H2
then the carrier of H1 c= the carrier of H2 by GROUP_2:def 5;
hence H1 "\/" H2 = gr (carr H2) by XBOOLE_1:12
.= H2 by Th31 ;
:: thesis: verum

end;

thus ( H1 "\/" H2 = H2 implies H1 is Subgroup of H2 ) by Th60; :: thesis: verum