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 )
A1: h1 "\/" h2 = (SubJoin G) . (h1,h2) by LATTICES:def 1;
assume A2: ( h1 = H1 & h2 = H2 ) ; :: thesis: h1 "\/" h2 = H1 "\/" H2
then ( H1 is strict & H2 is strict ) by GROUP_3:def 1;
hence h1 "\/" h2 = H1 "\/" H2 by A2, A1, GROUP_4:def 10; :: thesis: verum