let G be Group; :: thesis: 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 )
let H1, H2 be Subgroup of G; :: thesis: 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 )
let p, q be Element of (lattice G); :: thesis: ( p = H1 & q = H2 implies ( p [= q iff the carrier of H1 c= the carrier of H2 ) )
assume that
A1: p = H1 and
A2: q = H2 ; :: thesis: ( p [= q iff the carrier of H1 c= the carrier of H2 )
A3: H1 is strict Subgroup of G by A1, GROUP_3:def 1;
A4: H2 is strict Subgroup of G by A2, GROUP_3:def 1;
thus ( p [= q implies the carrier of H1 c= the carrier of H2 ) :: thesis: ( the carrier of H1 c= the carrier of H2 implies p [= q )

proof

assume p [= q ; :: thesis: the carrier of H1 c= the carrier of H2
then A5: p "/\" q = p by LATTICES:4;
p "/\" q = the L_meet of (lattice G) . (p,q) by LATTICES:def 2
.= H1 /\ H2 by A1, A2, A3, A4, GROUP_4:def 11 ;
then the carrier of H1 /\ the carrier of H2 = the carrier of H1 by A1, A5, Th1;
hence the carrier of H1 c= the carrier of H2 by XBOOLE_1:17; :: thesis: verum

end;

thus ( the carrier of H1 c= the carrier of H2 implies p [= q ) :: thesis: verum

proof

assume the carrier of H1 c= the carrier of H2 ; :: thesis: p [= q
then H1 is Subgroup of H2 by GROUP_2:57;
then A6: H1 /\ H2 = H1 by A3, GROUP_2:89;
H1 /\ H2 = the L_meet of (lattice G) . (p,q) by A1, A2, A3, A4, GROUP_4:def 11
.= p "/\" q by LATTICES:def 2 ;
hence p [= q by A1, A6, LATTICES:4; :: thesis: verum

end;