set x = the Element of Day A;
set y = the Element of Day 0;
born the Element of Day 0 c= 0 by SURREAL0:def 18;
then A1: born the Element of Day 0 = 0 ;
born the Element of Day A c= A by SURREAL0:def 18;
then (born the Element of Day A) (+) (born the Element of Day 0) c= A by A1, ORDINAL7:69;
hence not Triangle A is empty by Def5; :: thesis: verum