let o1, o2 be Ordinal; :: thesis: 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
let B be set ; :: thesis: ( ( for x being set holds
( x in B iff ex o being Ordinal st
( x = o1 +^ o & o in o2 ) ) ) implies o1 +^ o2 = o1 \/ B )
assume A1: for x being set holds
( x in B iff ex o being Ordinal st
( x = o1 +^ o & o in o2 ) ) ; :: thesis: o1 +^ o2 = o1 \/ B
for x being object holds
( x in o1 +^ o2 iff x in o1 \/ B )

proof

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

proof

assume A3: x in o1 \/ B ; :: thesis: x in o1 +^ o2

per cases ( x in o1 or x in B ) by A3, XBOOLE_0:def 3;

suppose A4: x in o1 ; :: thesis: x in o1 +^ o2

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

end;

suppose x in B ; :: thesis: x in o1 +^ o2

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

end;

end;

end;

per cases ( x in o1 or not x in o1 ) ;

suppose x in o1 ; :: thesis: ( x in o1 +^ o2 iff x in o1 \/ B )

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

end;

suppose A5: not x in o1 ; :: thesis: ( x in o1 +^ o2 iff x in o1 \/ B )

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

proof

assume A6: x in o1 +^ o2 ; :: thesis: x in o1 \/ B

per cases ( o2 = {} or o2 <> {} ) ;

suppose o2 = {} ; :: thesis: x in o1 \/ B

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

end;

suppose A7: o2 <> {} ; :: thesis: x in o1 \/ B

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: verum

end;

end;

end;

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

end;

end;

end;

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