:: deftheorem defines arithmetic WAYBEL_8:def 5 :
for L being non empty reflexive RelStr holds
( L is arithmetic iff ( L is algebraic & CompactSublatt L is meet-inheriting ) );