theorem :: SURREAL0:46

for X, Y being set
for A being Ordinal holds
( [X,Y] in Day A iff ( X << Y & ( for o being object st o in X \/ Y holds
ex O being Ordinal st
( O in A & o in Day O ) ) ) )