let G be Group; :: thesis: for H1, H2, K being Subgroup of G
for K1, K2 being Subgroup of K st multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of K1, the multF of K1 #) & multMagma(# the carrier of H2, the multF of H2 #) = multMagma(# the carrier of K2, the multF of K2 #) holds
H1 /\ H2 = K1 /\ K2
let H1, H2, K be Subgroup of G; :: thesis: for K1, K2 being Subgroup of K st multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of K1, the multF of K1 #) & multMagma(# the carrier of H2, the multF of H2 #) = multMagma(# the carrier of K2, the multF of K2 #) holds
H1 /\ H2 = K1 /\ K2
let K1, K2 be Subgroup of K; :: thesis: ( multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of K1, the multF of K1 #) & multMagma(# the carrier of H2, the multF of H2 #) = multMagma(# the carrier of K2, the multF of K2 #) implies H1 /\ H2 = K1 /\ K2 )
assume Z1: multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of K1, the multF of K1 #) ; :: thesis: ( not multMagma(# the carrier of H2, the multF of H2 #) = multMagma(# the carrier of K2, the multF of K2 #) or H1 /\ H2 = K1 /\ K2 )
assume Z2: multMagma(# the carrier of H2, the multF of H2 #) = multMagma(# the carrier of K2, the multF of K2 #) ; :: thesis: H1 /\ H2 = K1 /\ K2
Z3: K1 /\ K2 is Subgroup of G by GROUP_2:56;
Z4: for g being Element of G st g in H1 /\ H2 holds
g in K1 /\ K2

proof

let g be Element of G; :: thesis: ( g in H1 /\ H2 implies g in K1 /\ K2 )
assume g in H1 /\ H2 ; :: thesis: g in K1 /\ K2
then ( g in H1 & g in H2 ) by GROUP_2:82;
then ( g in K1 & g in K2 ) by Z1, Z2;
hence g in K1 /\ K2 by GROUP_2:82; :: thesis: verum

end;

for g being Element of G st g in K1 /\ K2 holds
g in H1 /\ H2

proof

let g be Element of G; :: thesis: ( g in K1 /\ K2 implies g in H1 /\ H2 )
assume g in K1 /\ K2 ; :: thesis: g in H1 /\ H2
then ( g in K1 & g in K2 ) by GROUP_2:82;
then ( g in H1 & g in H2 ) by Z1, Z2;
hence g in H1 /\ H2 by GROUP_2:82; :: thesis: verum

end;

hence H1 /\ H2 = K1 /\ K2 by Z3, Z4, GROUP_2:def 6; :: thesis: verum