thus
( ( for p, q being Element of Nat_Lattice holds p "\/" q = q "\/" p ) & ( for p, q, r being Element of Nat_Lattice holds p "\/" (q "\/" r) = (p "\/" q) "\/" r ) & ( for p, q being Element of Nat_Lattice holds (p "/\" q) "\/" q = q ) & ( for p, q being Element of Nat_Lattice holds p "/\" q = q "/\" p ) & ( for p, q, r being Element of Nat_Lattice holds p "/\" (q "/\" r) = (p "/\" q) "/\" r ) & ( for p, q being Element of Nat_Lattice holds p "/\" (p "\/" q) = p ) )
by NEWTON:43, NEWTON:48, NEWTON:53, NEWTON:54; LATTICES:def 4,LATTICES:def 5,LATTICES:def 6,LATTICES:def 7,LATTICES:def 8,LATTICES:def 9,LATTICES:def 10 verum