theorem :: ORDINAL3:59

for A, B, C being Ordinal st A c= B holds
A -^ C c= B -^ C