:: deftheorem defines atom WAYBEL15:def 1 :
for L being non empty RelStr
for a being Element of L holds
( a is atom iff ( Bottom L < a & ( for b being Element of L st Bottom L < b & b <= a holds
b = a ) ) );