theorem Eq0: :: LATWAL_2:34

for L being Lattice holds LattRel L = LatOrder L