let G be Group; :: thesis: for H1 being Subgroup of G
for H2 being strict Subgroup of G holds (H1 /\ H2) "\/" H2 = H2
let H1 be Subgroup of G; :: thesis: for H2 being strict Subgroup of G holds (H1 /\ H2) "\/" H2 = H2
let H2 be strict Subgroup of G; :: thesis: (H1 /\ H2) "\/" H2 = H2
H1 /\ H2 is Subgroup of H2 by GROUP_2:88;
hence (H1 /\ H2) "\/" H2 = H2 by Th61; :: thesis: verum