theorem Idem2: :: LATWAL_2:27

for L being WA_Lattice
for x, y being Element of L holds
( [x,y] in LatOrder L iff x [= y )