theorem :: YELLOW_4:8

for L being RelStr
for A, B being Subset of L st A is_coarser_than B & B is upper holds
A c= B