for L being Lattice holds
( L is finite iff L .: is finite ) ;