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