let X be set ; :: thesis: for x, y, z being Surreal st z = [{x,y},X] holds
[{x},X] is Surreal
let x, y, z be Surreal; :: thesis: ( z = [{x,y},X] implies [{x},X] is Surreal )
set b = born z;
assume A1: z = [{x,y},X] ; :: thesis: [{x},X] is Surreal
A2: z in Day (born z) by SURREAL0:def 18;
then A3: ( {x,y} << X & ( for o being object st o in {x,y} \/ X 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 l = x by TARSKI:def 1;
then l 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