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 H1 is Subgroup 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 H1 is Subgroup of H2 )
let p, q be Element of (lattice G); :: thesis: ( p = H1 & q = H2 implies ( p [= q iff H1 is Subgroup of H2 ) )
assume that
A1: p = H1 and
A2: q = H2 ; :: thesis: ( p [= q iff H1 is Subgroup of H2 )
thus ( p [= q implies H1 is Subgroup of H2 ) :: thesis: ( H1 is Subgroup of H2 implies p [= q )

proof

assume p [= q ; :: thesis: H1 is Subgroup of H2
then the carrier of H1 c= the carrier of H2 by A1, A2, Th25;
hence H1 is Subgroup of H2 by GROUP_2:57; :: thesis: verum

end;

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 ( H1 is Subgroup of H2 implies p [= q ) :: thesis: verum

proof

assume H1 is Subgroup of H2 ; :: thesis: p [= q
then A5: 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, A5, LATTICES:4; :: thesis: verum

end;