for S, T being lower-bounded LATTICE st [:S,T:] is arithmetic holds
( S is arithmetic & T is arithmetic )