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 Th9
.= hcflat . ((hcflat . (q,p)),r) by Th6 ; :: 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 Th6
.= hcflat . ((hcflat . (p,r)),q) by Th9 ; :: 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 Th6 ; :: thesis: hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,p)),q)
thus hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,p)),q) by A1, Th6; :: thesis: verum