set L = ExNearLattice ;
for x, y being Element of ExNearLattice holds x "/\" y = y "/\" x by Lemacik1;
hence ExNearLattice is meet-commutative by LATTICES:def 6; :: thesis: verum