let x be Surreal; :: thesis: for Inv being Function holds Union (divR (x,Inv)) = (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv))
let Inv be Function; :: thesis: Union (divR (x,Inv)) = (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv))
defpred S₁[ Nat] means (divR (x,Inv)) . $1 c= (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv));
(divR (x,Inv)) . 0 = {} by Th1;
then A1: S₁[ 0 ] by XBOOLE_1:2;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in (divR (x,Inv)) . (n + 1) or o in (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) )
assume A4: o in (divR (x,Inv)) . (n + 1) ; :: thesis: o in (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv))
(divR (x,Inv)) . (n + 1) = (((divR (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(L_ x),Inv))) \/ (divset (((divR (x,Inv)) . n),x,(R_ x),Inv)) by Th6;
then ( o in ((divR (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(L_ x),Inv)) or o in divset (((divR (x,Inv)) . n),x,(R_ x),Inv) ) by A4, XBOOLE_0:def 3;

per cases then ( o in (divR (x,Inv)) . n or o in divset (((divL (x,Inv)) . n),x,(L_ x),Inv) or o in divset (((divR (x,Inv)) . n),x,(R_ x),Inv) ) by XBOOLE_0:def 3;

suppose o in (divR (x,Inv)) . n ; :: thesis: o in (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv))

hence o in (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) by A3; :: thesis: verum

end;

suppose A5: o in divset (((divL (x,Inv)) . n),x,(L_ x),Inv) ; :: thesis: o in (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv))

divset (((divL (x,Inv)) . n),x,(L_ x),Inv) c= divset ((Union (divL (x,Inv))),x,(L_ x),Inv) by Th11, ABCMIZ_1:1;
hence o in (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) by A5, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A6: o in divset (((divR (x,Inv)) . n),x,(R_ x),Inv) ; :: thesis: o in (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv))

divset (((divR (x,Inv)) . n),x,(R_ x),Inv) c= divset ((Union (divR (x,Inv))),x,(R_ x),Inv) by Th11, ABCMIZ_1:1;
hence o in (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) by A6, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

A7: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
thus Union (divR (x,Inv)) c= (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) :: according to XBOOLE_0:def 10 :: thesis: (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) c= Union (divR (x,Inv))

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in Union (divR (x,Inv)) or o in (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) )
assume o in Union (divR (x,Inv)) ; :: thesis: o in (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv))
then consider n being object such that
A8: ( n in dom (divR (x,Inv)) & o in (divR (x,Inv)) . n ) by CARD_5:2;
n in NAT by A8, Def6;
then reconsider n = n as Nat ;
(divR (x,Inv)) . n c= (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) by A7;
hence o in (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) by A8; :: thesis: verum

end;

A9: divset ((Union (divL (x,Inv))),x,(L_ x),Inv) c= Union (divR (x,Inv))

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in divset ((Union (divL (x,Inv))),x,(L_ x),Inv) or o in Union (divR (x,Inv)) )
assume o in divset ((Union (divL (x,Inv))),x,(L_ x),Inv) ; :: thesis: o in Union (divR (x,Inv))
then consider l being object such that
A10: ( l in Union (divL (x,Inv)) & o in divs (l,x,(L_ x),Inv) ) by Def3;
consider n being object such that
A11: ( n in dom (divL (x,Inv)) & l in (divL (x,Inv)) . n ) by A10, CARD_5:2;
n in NAT by A11, Def5;
then reconsider n = n as Nat ;
o in divset (((divL (x,Inv)) . n),x,(L_ x),Inv) by A10, A11, Def3;
then o in ((divR (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(L_ x),Inv)) by XBOOLE_0:def 3;
then o in (((divR (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(L_ x),Inv))) \/ (divset (((divR (x,Inv)) . n),x,(R_ x),Inv)) by XBOOLE_0:def 3;
then A12: o in (divR (x,Inv)) . (n + 1) by Th6;
n + 1 in NAT ;
then n + 1 in dom (divR (x,Inv)) by Def6;
hence o in Union (divR (x,Inv)) by A12, CARD_5:2; :: thesis: verum

end;

divset ((Union (divR (x,Inv))),x,(R_ x),Inv) c= Union (divR (x,Inv))

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in divset ((Union (divR (x,Inv))),x,(R_ x),Inv) or o in Union (divR (x,Inv)) )
assume o in divset ((Union (divR (x,Inv))),x,(R_ x),Inv) ; :: thesis: o in Union (divR (x,Inv))
then consider l being object such that
A13: ( l in Union (divR (x,Inv)) & o in divs (l,x,(R_ x),Inv) ) by Def3;
consider n being object such that
A14: ( n in dom (divR (x,Inv)) & l in (divR (x,Inv)) . n ) by A13, CARD_5:2;
n in NAT by A14, Def6;
then reconsider n = n as Nat ;
o in divset (((divR (x,Inv)) . n),x,(R_ x),Inv) by A13, A14, Def3;
then o in (((divR (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(L_ x),Inv))) \/ (divset (((divR (x,Inv)) . n),x,(R_ x),Inv)) by XBOOLE_0:def 3;
then A15: o in (divR (x,Inv)) . (n + 1) by Th6;
n + 1 in NAT ;
then n + 1 in dom (divR (x,Inv)) by Def6;
hence o in Union (divR (x,Inv)) by A15, CARD_5:2; :: thesis: verum

end;

hence (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) c= Union (divR (x,Inv)) by A9, XBOOLE_1:8; :: thesis: verum