theorem Th1: :: EXCHSORT:1

for a, b being Ordinal
for x being set holds
( x in (a +^ b) \ a iff ex c being Ordinal st
( x = a +^ c & c in b ) )