theorem :: LATSUBGR:24

for G being Group
for p being Element of (lattice G)
for H being Subgroup of G st p = H holds
H is strict Subgroup of G by GROUP_3:def 1;