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

thus hcflat . (q,p) = p "/\" q by LATTICES:def 2

.= hcflat . (p,q) ; :: thesis: verum