theorem Th25: :: LATSUBGR:25

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 the carrier of H1 c= the carrier of H2 )