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 Th63
.= lcmlat . (lcmlat . q,p),r by Th61 ; :: 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 Th61
.= lcmlat . (lcmlat . p,r),q by Th63 ; :: 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 Th61 ; :: thesis: lcmlat . p,(lcmlat . q,r) = lcmlat . (lcmlat . r,p),q
thus lcmlat . p,(lcmlat . q,r) = lcmlat . (lcmlat . r,p),q by A1, Th61; :: thesis: verum