theorem :: YELLOW_4:3

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