theorem Th12: :: ORDINAL5:12

for a, b, c being Ordinal st 0 in a & exp (a,b) in exp (a,c) holds
b in c