theorem Th20: :: ZFREFLE1:20

for A, B being Ordinal st A is_cofinal_with B holds
B c= A