let q, p 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