let G be addGroup; :: thesis: for H being Subgroup of G holds (0). G is Subgroup of H
let H be Subgroup of G; :: thesis: (0). G is Subgroup of H
(0). G = (0). H by Th63;
hence (0). G is Subgroup of H ; :: thesis: verum