let a, b be Ordinal; :: thesis: for x being set holds
( x in (a +^ b) \ a iff ex c being Ordinal st
( x = a +^ c & c in b ) )
let x be set ; :: thesis: ( x in (a +^ b) \ a iff ex c being Ordinal st
( x = a +^ c & c in b ) )
A1: ( x in (a +^ b) \ a iff ( a c= x & x in a +^ b ) ) by ORDINAL6:5;
hereby :: thesis: ( ex c being Ordinal st
( x = a +^ c & c in b ) implies x in (a +^ b) \ a )
assume A2: 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 A1, A2, ORDINAL3:def 5; :: thesis: d in b
hence d in b by A2, ORDINAL3:22; :: thesis: verum
end;
given c being Ordinal such that A3: ( x = a +^ c & c in b ) ; :: thesis: x in (a +^ b) \ a
( a c= x & x in a +^ b ) by A3, ORDINAL2:32, ORDINAL3:24;
hence x in (a +^ b) \ a by ORDINAL6:5; :: thesis: verum