theorem :: WAYBEL13:14

for S being lower-bounded LATTICE holds InclPoset (Ids S) is arithmetic