let A be Ordinal; :: thesis: ( [{},(Day A)] in (Day (succ A)) \ (Day A) & [(Day A),{}] in (Day (succ A)) \ (Day A) )
A1: ( {} << Day A & Day A << {} ) ;
for o being object st o in {} \/ (Day A) holds
ex O being Ordinal st
( O in succ A & o in Day O ) by ORDINAL1:6;
then A2: ( [{},(Day A)] in Day (succ A) & [(Day A),{}] in Day (succ A) ) by A1, SURREAL0:46;
then reconsider eD = [{},(Day A)], De = [(Day A),{}] as Surreal ;
A3: ( eD <= eD & De <= De ) ;
A4: ( eD in {eD} & De in {De} ) by TARSKI:def 1;
( L_ De << {De} & {eD} << R_ eD ) by Th11;
then ( not eD in Day A & not De in Day A ) by A3, A4;
hence ( [{},(Day A)] in (Day (succ A)) \ (Day A) & [(Day A),{}] in (Day (succ A)) \ (Day A) ) by A2, XBOOLE_0:def 5; :: thesis: verum