let G be Group; :: thesis: for H1, H2 being Subgroup of G
for h1, h2 being Element of (lattice G) st h1 = H1 & h2 = H2 holds
h1 "/\" h2 = H1 /\ H2
let H1, H2 be Subgroup of G; :: thesis: for h1, h2 being Element of (lattice G) st h1 = H1 & h2 = H2 holds
h1 "/\" h2 = H1 /\ H2
let h1, h2 be Element of (lattice G); :: thesis: ( h1 = H1 & h2 = H2 implies h1 "/\" h2 = H1 /\ H2 )
assume A0: ( h1 = H1 & h2 = H2 ) ; :: thesis: h1 "/\" h2 = H1 /\ H2
then A2: ( H1 is strict & H2 is strict ) by GROUP_3:def 1;
h1 "/\" h2 = (SubMeet G) . h1,h2 by LATTICES:def 2;
hence h1 "/\" h2 = H1 /\ H2 by A0, A2, GROUP_4:def 12; :: thesis: verum