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

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