let G be addGroup; :: thesis: for H1, H2 being Subgroup of G holds (0). H1 = (0). H2
let H1, H2 be Subgroup of G; :: thesis: (0). H1 = (0). H2
thus (0). H1 = (0). G by Th63
.= (0). H2 by Th63 ; :: thesis: verum