theorem :: YELLOW_4:7

for L being transitive RelStr
for A, B, C being Subset of L st C is_coarser_than B & B is_coarser_than A holds
C is_coarser_than A