theorem Eq2: :: LATWAL_2:36

for L being WA-Lattice
for a, b being Element of L
for aa, bb being Element of (wlatt L) st a = aa & b = bb holds
( aa [= bb iff a <= b )