theorem :: NAT_LAT:10

for p, q, r being Element of Nat_Lattice holds
( 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) )