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