theorem
for
p,
q,
r being
Element of
Nat_Lattice holds
(
lcmlat . (
p,
(lcmlat . (q,r)))
= lcmlat . (
(lcmlat . (q,p)),
r) &
lcmlat . (
p,
(lcmlat . (q,r)))
= lcmlat . (
(lcmlat . (p,r)),
q) &
lcmlat . (
p,
(lcmlat . (q,r)))
= lcmlat . (
(lcmlat . (r,q)),
p) &
lcmlat . (
p,
(lcmlat . (q,r)))
= lcmlat . (
(lcmlat . (r,p)),
q) )