theorem :: LATSUBGR:26

for G being Group
for H1, H2 being Subgroup of G
for p, q being Element of (lattice G) st p = H1 & q = H2 holds
( p [= q iff H1 is Subgroup of H2 )