:: deftheorem defines is_finer_than YELLOW_4:def 1 :
for L being RelStr
for A, B being Subset of L holds
( A is_finer_than B iff for a being Element of L st a in A holds
ex b being Element of L st
( b in B & a <= b ) );