theorem Th5: :: LATTICE5:5

for A being set
for x, y being Element of (EqRelLatt A) holds
( x [= y iff x c= y )