for A, B being Ordinal st A is_cofinal_with B & B is_cofinal_with A holds
A = B by Th20;