let X be set ; :: thesis: for x, y, z being Surreal st z = [X,{x,y}] holds
[X,{x}] is Surreal
let x, y, z be Surreal; :: thesis: ( z = [X,{x,y}] implies [X,{x}] is Surreal )
set b = born z;
assume A1: z = [X,{x,y}] ; :: thesis: [X,{x}] is Surreal
A2: z in Day (born z) by SURREAL0:def 18;
then A3: ( X << {x,y} & ( for o being object st o in X \/ {x,y} holds
ex O being Ordinal st
( O in born z & o in Day O ) ) ) by A1, SURREAL0:46;
A4: X << {x}

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis: for b₁ being set holds
( not l in X or not b₁ in {x} or not l >= b₁ )
let r be Surreal; :: thesis: ( not l in X or not r in {x} or not l >= r )
assume A5: ( l in X & r in {x} ) ; :: thesis: not l >= r
then r = x by TARSKI:def 1;
then r in {x,y} by TARSKI:def 2;
hence not l >= r by A3, A5; :: thesis: verum

end;

for o being object st o in X \/ {x} holds
ex O being Ordinal st
( O in born z & o in Day O )

proof

let o be object ; :: thesis: ( o in X \/ {x} implies ex O being Ordinal st
( O in born z & o in Day O ) )
assume o in X \/ {x} ; :: thesis: ex O being Ordinal st
( O in born z & o in Day O )
then ( o in {x} or o in X ) by XBOOLE_0:def 3;
then ( o = x or o in X ) by TARSKI:def 1;
then ( o in {x,y} or o in X ) by TARSKI:def 2;
then o in {x,y} \/ X by XBOOLE_0:def 3;
hence ex O being Ordinal st
( O in born z & o in Day O ) by A2, A1, SURREAL0:46; :: thesis: verum

end;

then [X,{x}] in Day (born z) by A4, SURREAL0:46;
hence [X,{x}] is Surreal ; :: thesis: verum