let o be object ; :: thesis: for p being pair object holds Union (sqrtL (p,o)) = (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))))
let p be pair object ; :: thesis: Union (sqrtL (p,o)) = (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))))
defpred S₁[ Nat] means (sqrtL (p,o)) . $1 c= (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))));
(sqrtL (p,o)) . 0 = L_ p by Th6;
then A1: S₁[ 0 ] by XBOOLE_1:7;
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 a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (sqrtL (p,o)) . (n + 1) or a in (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o))))) )
assume A4: a in (sqrtL (p,o)) . (n + 1) ; :: thesis: a in (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))))
(sqrtL (p,o)) . (n + 1) = ((sqrtL (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtR (p,o)) . n))) by Th8;

per cases then ( a in (sqrtL (p,o)) . n or a in sqrt (o,((sqrtL (p,o)) . n),((sqrtR (p,o)) . n)) ) by XBOOLE_0:def 3, A4;

suppose a in (sqrtL (p,o)) . n ; :: thesis: a in (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))))

hence a in (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o))))) by A3; :: thesis: verum

end;

suppose A5: a in sqrt (o,((sqrtL (p,o)) . n),((sqrtR (p,o)) . n)) ; :: thesis: a in (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))))

( (sqrtL (p,o)) . n c= Union (sqrtL (p,o)) & (sqrtR (p,o)) . n c= Union (sqrtR (p,o)) ) by ABCMIZ_1:1;
then sqrt (o,((sqrtL (p,o)) . n),((sqrtR (p,o)) . n)) c= sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))) by Th11;
hence a in (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o))))) by A5, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

A6: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
thus Union (sqrtL (p,o)) c= (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o))))) :: according to XBOOLE_0:def 10 :: thesis: (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o))))) c= Union (sqrtL (p,o))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Union (sqrtL (p,o)) or a in (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o))))) )
assume a in Union (sqrtL (p,o)) ; :: thesis: a in (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))))
then consider n being object such that
A7: ( n in dom (sqrtL (p,o)) & a in (sqrtL (p,o)) . n ) by CARD_5:2;
n in NAT by A7, Def4;
then reconsider n = n as Nat ;
(sqrtL (p,o)) . n c= (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o))))) by A6;
hence a in (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o))))) by A7; :: thesis: verum

end;

A8: sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))) c= Union (sqrtL (p,o))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))) or a in Union (sqrtL (p,o)) )
assume a in sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))) ; :: thesis: a in Union (sqrtL (p,o))
then consider x1, y1 being Surreal such that
A9: ( x1 in Union (sqrtL (p,o)) & y1 in Union (sqrtR (p,o)) & not x1 + y1 == 0_No & a = (o +' (x1 * y1)) * ((x1 + y1) ") ) by Def2;
consider n being object such that
A10: ( n in dom (sqrtL (p,o)) & x1 in (sqrtL (p,o)) . n ) by A9, CARD_5:2;
consider m being object such that
A11: ( m in dom (sqrtR (p,o)) & y1 in (sqrtR (p,o)) . m ) by A9, CARD_5:2;
( n in NAT & m in NAT ) by A11, A10, Def4, Def5;
then reconsider n = n, m = m as Nat ;
set nm = n + m;
( m <= n + m & n <= n + m ) by NAT_1:11;
then ( (sqrtL (p,o)) . n c= (sqrtL (p,o)) . (n + m) & (sqrtR (p,o)) . m c= (sqrtR (p,o)) . (n + m) ) by Th7;
then A12: a in sqrt (o,((sqrtL (p,o)) . (n + m)),((sqrtR (p,o)) . (n + m))) by A9, A10, A11, Def2;
(sqrtL (p,o)) . ((n + m) + 1) = ((sqrtL (p,o)) . (n + m)) \/ (sqrt (o,((sqrtL (p,o)) . (n + m)),((sqrtR (p,o)) . (n + m)))) by Th8;
then A13: a in (sqrtL (p,o)) . ((n + m) + 1) by A12, XBOOLE_0:def 3;
(n + m) + 1 in NAT ;
then (n + m) + 1 in dom (sqrtL (p,o)) by Def4;
hence a in Union (sqrtL (p,o)) by A13, CARD_5:2; :: thesis: verum

end;

L_ p = (sqrtL (p,o)) . 0 by Th6;
then L_ p c= Union (sqrtL (p,o)) by ABCMIZ_1:1;
hence (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o))))) c= Union (sqrtL (p,o)) by A8, XBOOLE_1:8; :: thesis: verum