let IT1, IT2 be Subset of [:(Day A),(Day A):]; :: thesis: ( ( for x, y being Surreal holds
( [x,y] in IT1 iff (born x) (+) (born y) c= A ) ) & ( for x, y being Surreal holds
( [x,y] in IT2 iff (born x) (+) (born y) c= A ) ) implies IT1 = IT2 )
assume that
A4: for x, y being Surreal holds
( [x,y] in IT1 iff (born x) (+) (born y) c= A ) and
A5: for x, y being Surreal holds
( [x,y] in IT2 iff (born x) (+) (born y) c= A ) ; :: thesis: IT1 = IT2
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in IT1 or [x,y] in IT2 ) & ( not [x,y] in IT2 or [x,y] in IT1 ) )
thus ( [x,y] in IT1 implies [x,y] in IT2 ) :: thesis: ( not [x,y] in IT2 or [x,y] in IT1 )

proof

assume A6: [x,y] in IT1 ; :: thesis: [x,y] in IT2
then reconsider x1 = x, y1 = y as Element of Day A by ZFMISC_1:87;
(born x1) (+) (born y1) c= A by A6, A4;
hence [x,y] in IT2 by A5; :: thesis: verum

end;

assume A7: [x,y] in IT2 ; :: thesis: [x,y] in IT1
then reconsider x1 = x, y1 = y as Element of Day A by ZFMISC_1:87;
(born x1) (+) (born y1) c= A by A7, A5;
hence [x,y] in IT1 by A4; :: thesis: verum