theorem :: SURREALO:36

for A being Ordinal holds
( [{},(Day A)] in (Day (succ A)) \ (Day A) & [(Day A),{}] in (Day (succ A)) \ (Day A) )