theorem LemmaEqual0: :: LATWAL_2:29

for L being WA_Lattice
for x, y being Element of L
for xx, yy being Element of (LatRelStr L) st x = xx & y = yy holds
( x [= y iff xx <= yy )