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