let p, q, r be Element of Nat_Lattice ; :: thesis: ( hcflat . p,(hcflat . q,r) = hcflat . (hcflat . q,p),r & hcflat . p,(hcflat . q,r) = hcflat . (hcflat . p,r),q & hcflat . p,(hcflat . q,r) = hcflat . (hcflat . r,q),p & hcflat . p,(hcflat . q,r) = hcflat . (hcflat . r,p),q )
set s = r "/\" q;
thus hcflat . p,(hcflat . q,r) = hcflat . (hcflat . p,q),r by Th65
.= hcflat . (hcflat . q,p),r by Th62 ; :: thesis: ( hcflat . p,(hcflat . q,r) = hcflat . (hcflat . p,r),q & hcflat . p,(hcflat . q,r) = hcflat . (hcflat . r,q),p & hcflat . p,(hcflat . q,r) = hcflat . (hcflat . r,p),q )
thus A1: hcflat . p,(hcflat . q,r) = hcflat . p,(hcflat . r,q) by Th62
.= hcflat . (hcflat . p,r),q by Th65 ; :: thesis: ( hcflat . p,(hcflat . q,r) = hcflat . (hcflat . r,q),p & hcflat . p,(hcflat . q,r) = hcflat . (hcflat . r,p),q )
thus hcflat . p,(hcflat . q,r) = hcflat . p,(r "/\" q) by LATTICES:def 2
.= hcflat . (hcflat . r,q),p by Th62 ; :: thesis: hcflat . p,(hcflat . q,r) = hcflat . (hcflat . r,p),q
thus hcflat . p,(hcflat . q,r) = hcflat . (hcflat . r,p),q by A1, Th62; :: thesis: verum