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