let p, q be Element of Nat_Lattice; :: thesis: hcflat . (q,p) = hcflat . (p,q)
thus hcflat . (q,p) = p "/\" q by LATTICES:def 2
.= hcflat . (p,q) ; :: thesis: verum