theorem Th1: :: POLYNOM6:1

for o1, o2 being Ordinal
for B being set st ( for x being set holds
( x in B iff ex o being Ordinal st
( x = o1 +^ o & o in o2 ) ) ) holds
o1 +^ o2 = o1 \/ B