theorem :: LATTICE3:11

for L being Lattice holds
( LattPOSet L is with_suprema & LattPOSet L is with_infima )