theorem Eq1: :: LATWAL_2:35

for L being with_suprema with_infima Poset
for a, b being Element of L
for aa, bb being Element of (latt L) st a = aa & b = bb holds
( aa [= bb iff a <= b )