theorem :: LATTICE3:20

for L being Lattice holds
( (LattRel L) ~ = LattRel (L .:) & (LattPOSet L) ~ = LattPOSet (L .:) )