let p, q, r be Element of Nat_Lattice; :: thesis: ( 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) )
set s = r "\/" q;
thus lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (p,q)),r) by Th7
.= lcmlat . ((lcmlat . (q,p)),r) by Th5 ; :: thesis: ( 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) )
thus A1: lcmlat . (p,(lcmlat . (q,r))) = lcmlat . (p,(lcmlat . (r,q))) by Th5
.= lcmlat . ((lcmlat . (p,r)),q) by Th7 ; :: thesis: ( lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,q)),p) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,p)),q) )
thus lcmlat . (p,(lcmlat . (q,r))) = lcmlat . (p,(r "\/" q)) by LATTICES:def 1
.= lcmlat . ((lcmlat . (r,q)),p) by Th5 ; :: thesis: lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,p)),q)
thus lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,p)),q) by A1, Th5; :: thesis: verum