let o1, o2 be Ordinal; :: thesis:
let B be set ; :: thesis:
assume A1: for x being set holds
( x in B iff ex o being Ordinal st
( x = o1 +^ o & o in o2 ) ) ; :: thesis:
for x being object holds
( x in o1 +^ o2 iff x in o1 \/ B )

proof

let x be object ; :: thesis:
A2: ( x in o1 \/ B implies x in o1 +^ o2 )

proof

assume A3: x in o1 \/ B ; :: thesis:

per cases by A3, XBOOLE_0:def 3;

suppose A4: x in o1 ; :: thesis:

o1 c= o1 +^ o2 by ORDINAL3:24;
hence x in o1 +^ o2 by A4; :: thesis:

end;

suppose x in B ; :: thesis:

then ex o being Ordinal st
( x = o1 +^ o & o in o2 ) by A1;
hence x in o1 +^ o2 by ORDINAL2:32; :: thesis:

end;

end;

end;

per cases ;

suppose x in o1 ; :: thesis:

hence ( x in o1 +^ o2 implies x in o1 \/ B ) by XBOOLE_0:def 3; :: thesis:
thus ( x in o1 \/ B implies x in o1 +^ o2 ) by A2; :: thesis:

end;

suppose A5: not x in o1 ; :: thesis:

thus ( x in o1 +^ o2 implies x in o1 \/ B ) :: thesis:

proof

assume A6: x in o1 +^ o2 ; :: thesis:

per cases ;

suppose o2 = {} ; :: thesis:

hence x in o1 \/ B by A5, A6, ORDINAL2:27; :: thesis:

end;

suppose A7: o2 <> {} ; :: thesis:

reconsider o = x as Ordinal by A6;
o1 c= o by A5, ORDINAL1:16;
then A8: o = o1 +^ (o -^ o1) by ORDINAL3:def 5;
o -^ o1 in o2 by A6, A7, ORDINAL3:60;
then x in B by A1, A8;
hence x in o1 \/ B by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

thus ( x in o1 \/ B implies x in o1 +^ o2 ) by A2; :: thesis:

end;

end;

end;

hence o1 +^ o2 = o1 \/ B by TARSKI:2; :: thesis: