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