let r be Real; :: thesis: sReal . r == real_qua (sReal . r)
set R = sReal . r;
uReal . r = Unique_No (sReal . r) by Def7;
then A1: uReal . r == sReal . r by SURREALO:def 10;
A2: L_ (sReal . r) << {(real_qua (sReal . r))}

proof

let l, r1 be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in L_ (sReal . r) or not r1 in {(real_qua (sReal . r))} or not r1 <= l )
assume A3: ( l in L_ (sReal . r) & r1 in {(real_qua (sReal . r))} ) ; :: thesis: not r1 <= l
then consider n being Nat such that
A4: l = uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) by Th42;
set D = [/((r * (2 |^ n)) - 1)\] / (2 |^ n);
0 < r - ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) by XREAL_1:50, Th41;
then consider k being Nat such that
A5: 1 / (2 |^ k) <= r - ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) by PREPOWER:92;
[/((r * (2 |^ n)) - 1)\] / (2 |^ n) <= r - (1 / (2 |^ k)) by A5, XREAL_1:11;
then ( l = uReal . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) & uReal . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) <= uReal . (r + (- (1 / (2 |^ k)))) & uReal . (r + (- (1 / (2 |^ k)))) == (uReal . r) + (uReal . (- (1 / (2 |^ k)))) ) by Th46, A4, Th51, Th55;
then A6: l <= (uReal . r) + (uReal . (- (1 / (2 |^ k)))) by SURREALO:4;
( uReal . (- (1 / (2 |^ k))) == - (uReal . (1 / (2 |^ k))) & - (uReal . (1 / (2 |^ k))) == - ((uInt . (2 |^ k)) ") ) by Th58, Th56, SURREALR:65;
then uReal . (- (1 / (2 |^ k))) == - ((uInt . (2 |^ k)) ") by SURREALO:4;
then (uReal . r) + (uReal . (- (1 / (2 |^ k)))) == (sReal . r) + (- ((uInt . (2 |^ k)) ")) by A1, SURREALR:66;
then ( l <= (sReal . r) - ((uInt . (2 |^ k)) ") & (sReal . r) - ((uInt . (2 |^ k)) ") < real_qua (sReal . r) & real_qua (sReal . r) = r1 ) by A3, TARSKI:def 1, Th59, A6, SURREALO:4;
hence not r1 <= l by SURREALO:4; :: thesis: verum

end;

A7: {(sReal . r)} << R_ (real_qua (sReal . r))

proof

let l, r1 be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in {(sReal . r)} or not r1 in R_ (real_qua (sReal . r)) or not r1 <= l )
assume A8: ( l in {(sReal . r)} & r1 in R_ (real_qua (sReal . r)) ) ; :: thesis: not r1 <= l
r1 in { ((sReal . r) + ((uInt . n) ")) where n is positive Nat : verum } by A8, Def8;
then consider nL being positive Nat such that
A9: r1 = (sReal . r) + ((uInt . nL) ") ;
( sReal . r = (sReal . r) + 0_No & (sReal . r) + 0_No < (sReal . r) + ((uInt . nL) ") ) by SURREALR:44, SURREALI:def 8;
hence not r1 <= l by A9, A8, TARSKI:def 1; :: thesis: verum

end;

A10: L_ (real_qua (sReal . r)) << {(sReal . r)}

proof

let l, r1 be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in L_ (real_qua (sReal . r)) or not r1 in {(sReal . r)} or not r1 <= l )
assume A11: ( l in L_ (real_qua (sReal . r)) & r1 in {(sReal . r)} ) ; :: thesis: not r1 <= l
l in { ((sReal . r) - ((uInt . n) ")) where n is positive Nat : verum } by A11, Def8;
then consider nL being positive Nat such that
A12: l = (sReal . r) - ((uInt . nL) ") ;
( - ((uInt . nL) ") < - 0_No & - 0_No = 0_No ) by SURREALR:10, SURREALI:def 8;
then ( (sReal . r) + (- ((uInt . nL) ")) < (sReal . r) + 0_No & (sReal . r) + 0_No = sReal . r ) by SURREALR:44;
hence not r1 <= l by A12, A11, TARSKI:def 1; :: thesis: verum

end;

{(real_qua (sReal . r))} << R_ (sReal . r)

proof

let r1, l be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not r1 in {(real_qua (sReal . r))} or not l in R_ (sReal . r) or not l <= r1 )
assume A13: ( r1 in {(real_qua (sReal . r))} & l in R_ (sReal . r) ) ; :: thesis: not l <= r1
then consider n being Nat such that
A14: l = uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n)) by Th43;
set D = [\((r * (2 |^ n)) + 1)/] / (2 |^ n);
0 < ([\((r * (2 |^ n)) + 1)/] / (2 |^ n)) - r by Th41, XREAL_1:50;
then consider k being Nat such that
A15: 1 / (2 |^ k) <= ([\((r * (2 |^ n)) + 1)/] / (2 |^ n)) - r by PREPOWER:92;
( l = uReal . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n)) & uReal . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n)) >= uReal . (r + (1 / (2 |^ k))) & uReal . (r + (1 / (2 |^ k))) == (uReal . r) + (uReal . (1 / (2 |^ k))) ) by A14, A15, XREAL_1:19, Th46, Th51, Th55;
then A16: l >= (uReal . r) + (uReal . (1 / (2 |^ k))) by SURREALO:4;
uReal . (1 / (2 |^ k)) == (uInt . (2 |^ k)) " by Th58;
then (uReal . r) + (uReal . (1 / (2 |^ k))) == (sReal . r) + ((uInt . (2 |^ k)) ") by A1, SURREALR:66;
then ( r1 = real_qua (sReal . r) & real_qua (sReal . r) < (sReal . r) + ((uInt . (2 |^ k)) ") & (sReal . r) + ((uInt . (2 |^ k)) ") <= l ) by A13, TARSKI:def 1, Th59, A16, SURREALO:4;
hence not l <= r1 by SURREALO:4; :: thesis: verum

end;

hence sReal . r == real_qua (sReal . r) by A2, A7, A10, SURREAL0:43; :: thesis: verum