for L being RelStr
for B being Subset of L holds {} L is_finer_than B ;