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