for L being non empty reflexive RelStr
for A, B being Subset of L st A c= B holds
( A is_finer_than B & A is_coarser_than B )