theorem :: YELLOW_4:6

for L being RelStr
for A being Subset of L holds {} L is_coarser_than A ;