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