let x be Surreal; :: thesis: - x = [(-- (R_ x)),(-- (L_ x))]
set A = born x;
consider S being Function-yielding c=-monotone Sequence such that
A1: ( dom S = succ (born x) & No_opposite_op (born x) = S . (born x) ) and
A2: for B being Ordinal st B in succ (born x) holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for x being object st x in Day B holds
SB . x = [((union (rng (S | B))) .: (R_ x)),((union (rng (S | B))) .: (L_ x))] ) ) by Def2;
consider SA being ManySortedSet of Day (born x) such that
A3: S . (born x) = SA and
A4: for x being object st x in Day (born x) holds
SA . x = [((union (rng (S | (born x)))) .: (R_ x)),((union (rng (S | (born x)))) .: (L_ x))] by A2, ORDINAL1:6;
set U = union (rng (S | (born x)));
x in Day (born x) by SURREAL0:def 18;
then A5: [((union (rng (S | (born x)))) .: (R_ x)),((union (rng (S | (born x)))) .: (L_ x))] = - x by A1, A3, A4;
A6: -- (R_ x) c= (union (rng (S | (born x)))) .: (R_ x)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in -- (R_ x) or y in (union (rng (S | (born x)))) .: (R_ x) )
assume A7: y in -- (R_ x) ; :: thesis: y in (union (rng (S | (born x)))) .: (R_ x)
consider a being Surreal such that
A8: ( a in R_ x & y = - a ) by Def4, A7;
set B = born a;
A9: a in (L_ x) \/ (R_ x) by A8, XBOOLE_0:def 3;
then A10: born a in born x by SURREALO:1;
A11: born a in succ (born x) by A9, SURREALO:1, ORDINAL1:8;
then consider SB being ManySortedSet of Day (born a) such that
A12: S . (born a) = SB and
for x being object st x in Day (born a) holds
SB . x = [((union (rng (S | (born a)))) .: (R_ x)),((union (rng (S | (born a)))) .: (L_ x))] by A2;
A13: No_opposite_op (born a) = S . (born a) by A11, A1, A2, Th4;
A14: dom SB = Day (born a) by PARTFUN1:def 2;
A15: a in Day (born a) by SURREAL0:def 18;
A16: SB . a = (union (rng S)) . a by Th2, A12, A14, A15, A11, A1;
( (union (rng S)) . a = (union (rng (S | (born x)))) . a & a in dom (union (rng (S | (born x)))) ) by Th5, A10, A14, A15, A12;
hence y in (union (rng (S | (born x)))) .: (R_ x) by FUNCT_1:def 6, A8, A16, A13, A12; :: thesis: verum

end;

(union (rng (S | (born x)))) .: (R_ x) c= -- (R_ x)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (union (rng (S | (born x)))) .: (R_ x) or y in -- (R_ x) )
assume A17: y in (union (rng (S | (born x)))) .: (R_ x) ; :: thesis: y in -- (R_ x)
consider a being object such that
A18: ( a in dom (union (rng (S | (born x)))) & a in R_ x & (union (rng (S | (born x)))) . a = y ) by A17, FUNCT_1:def 6;
reconsider a = a as Surreal by A18, SURREAL0:def 16;
set B = born a;
A19: a in (L_ x) \/ (R_ x) by A18, XBOOLE_0:def 3;
then A20: born a in born x by SURREALO:1;
A21: born a in succ (born x) by SURREALO:1, A19, ORDINAL1:8;
then consider SB being ManySortedSet of Day (born a) such that
A22: S . (born a) = SB and
for x being object st x in Day (born a) holds
SB . x = [((union (rng (S | (born a)))) .: (R_ x)),((union (rng (S | (born a)))) .: (L_ x))] by A2;
A23: No_opposite_op (born a) = S . (born a) by A21, A1, A2, Th4;
A24: dom SB = Day (born a) by PARTFUN1:def 2;
A25: a in Day (born a) by SURREAL0:def 18;
SB . a = (union (rng S)) . a by Th2, A24, A25, A21, A22, A1;
then - a = y by A18, Th5, A20, A23, A24, A25, A22;
hence y in -- (R_ x) by A18, Def4; :: thesis: verum

end;

then A26: (union (rng (S | (born x)))) .: (R_ x) = -- (R_ x) by A6, XBOOLE_0:def 10;
A27: -- (L_ x) c= (union (rng (S | (born x)))) .: (L_ x)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in -- (L_ x) or y in (union (rng (S | (born x)))) .: (L_ x) )
assume A28: y in -- (L_ x) ; :: thesis: y in (union (rng (S | (born x)))) .: (L_ x)
consider a being Surreal such that
A29: ( a in L_ x & y = - a ) by Def4, A28;
set B = born a;
A30: a in (L_ x) \/ (R_ x) by A29, XBOOLE_0:def 3;
then A31: born a in born x by SURREALO:1;
A32: born a in succ (born x) by A30, SURREALO:1, ORDINAL1:8;
then consider SB being ManySortedSet of Day (born a) such that
A33: S . (born a) = SB and
for x being object st x in Day (born a) holds
SB . x = [((union (rng (S | (born a)))) .: (R_ x)),((union (rng (S | (born a)))) .: (L_ x))] by A2;
A34: No_opposite_op (born a) = S . (born a) by A32, A1, A2, Th4;
A35: dom SB = Day (born a) by PARTFUN1:def 2;
A36: a in Day (born a) by SURREAL0:def 18;
A37: SB . a = (union (rng S)) . a by Th2, A33, A35, A36, A32, A1;
( (union (rng S)) . a = (union (rng (S | (born x)))) . a & a in dom (union (rng (S | (born x)))) ) by Th5, A31, A35, A36, A33;
hence y in (union (rng (S | (born x)))) .: (L_ x) by FUNCT_1:def 6, A29, A37, A34, A33; :: thesis: verum

end;

(union (rng (S | (born x)))) .: (L_ x) c= -- (L_ x)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (union (rng (S | (born x)))) .: (L_ x) or y in -- (L_ x) )
assume A38: y in (union (rng (S | (born x)))) .: (L_ x) ; :: thesis: y in -- (L_ x)
consider a being object such that
A39: ( a in dom (union (rng (S | (born x)))) & a in L_ x & (union (rng (S | (born x)))) . a = y ) by A38, FUNCT_1:def 6;
reconsider a = a as Surreal by A39, SURREAL0:def 16;
set B = born a;
A40: a in (L_ x) \/ (R_ x) by A39, XBOOLE_0:def 3;
then A41: born a in born x by SURREALO:1;
A42: born a in succ (born x) by SURREALO:1, A40, ORDINAL1:8;
then consider SB being ManySortedSet of Day (born a) such that
A43: S . (born a) = SB and
for x being object st x in Day (born a) holds
SB . x = [((union (rng (S | (born a)))) .: (R_ x)),((union (rng (S | (born a)))) .: (L_ x))] by A2;
A44: No_opposite_op (born a) = S . (born a) by A42, A1, A2, Th4;
A45: dom SB = Day (born a) by PARTFUN1:def 2;
A46: a in Day (born a) by SURREAL0:def 18;
SB . a = (union (rng S)) . a by Th2, A45, A46, A42, A43, A1;
then - a = y by A39, Th5, A41, A44, A45, A46, A43;
hence y in -- (L_ x) by A39, Def4; :: thesis: verum

end;

hence - x = [(-- (R_ x)),(-- (L_ x))] by A5, A26, A27, XBOOLE_0:def 10; :: thesis: verum