let a, b be ordinal number ; :: thesis: for x being set holds
( x in (a +^ b) \ a iff ex c being ordinal number st
( x = a +^ c & c in b ) )
let x be set ; :: thesis: ( x in (a +^ b) \ a iff ex c being ordinal number st
( x = a +^ c & c in b ) )
A0: ( x in (a +^ b) \ a iff ( a c= x & x in a +^ b ) ) by ORDINAL6:5;

hereby :: thesis: ( ex c being ordinal number st
( x = a +^ c & c in b ) implies x in (a +^ b) \ a )

assume Z0: x in (a +^ b) \ a ; :: thesis: ex d being set st
( x = a +^ d & d in b )
then reconsider c = x as Ordinal ;
take d = c -^ a; :: thesis: ( x = a +^ d & d in b )
thus x = a +^ d by A0, Z0, ORDINAL3:def 5; :: thesis: d in b
hence d in b by Z0, ORDINAL3:22; :: thesis: verum

end;

given c being ordinal number such that Z1: ( x = a +^ c & c in b ) ; :: thesis: x in (a +^ b) \ a
( a c= x & x in a +^ b ) by Z1, ORDINAL2:32, ORDINAL3:24;
hence x in (a +^ b) \ a by ORDINAL6:5; :: thesis: verum