let G be Group; :: thesis: for H1, H2 being Subgroup of G holds (1). H1 = (1). H2
let H1, H2 be Subgroup of G; :: thesis: (1). H1 = (1). H2
thus (1). H1 = (1). G by Th75
.= (1). H2 by Th75 ; :: thesis: verum