let x, y be Surreal; :: thesis: ( x <= y iff for A being Ordinal st x in Day A & y in Day A holds
x <= No_Ord A,y )
consider Ax being Ordinal such that
A1: x in Day Ax by Def14;
consider Ay being Ordinal such that
A2: y in Day Ay by Def14;
thus ( x <= y implies for A being Ordinal st x in Day A & y in Day A holds
x <= No_Ord A,y ) by Th39; :: thesis: ( ( for A being Ordinal st x in Day A & y in Day A holds
x <= No_Ord A,y ) implies x <= y )
assume A3: for A being Ordinal st x in Day A & y in Day A holds
x <= No_Ord A,y ; :: thesis: x <= y
set A = Ax \/ Ay;
( Day Ax c= Day (Ax \/ Ay) & Day Ay c= Day (Ax \/ Ay) ) by Th35, XBOOLE_1:7;
hence x <= y by A1, A2, A3; :: thesis: verum