for A, B, C being Ordinal st A is_cofinal_with B & B is_cofinal_with C holds
A is_cofinal_with C by ORDINAL4:37;