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