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