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