set IT = { [x,y] where x, y is Element of Day A : (born x) (+) (born y) c= A } ;
{ [x,y] where x, y is Element of Day A : (born x) (+) (born y) c= A } c= [:(Day A),(Day A):]

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [x,y] where x, y is Element of Day A : (born x) (+) (born y) c= A } or a in [:(Day A),(Day A):] )
assume a in { [x,y] where x, y is Element of Day A : (born x) (+) (born y) c= A } ; :: thesis: a in [:(Day A),(Day A):]
then ex x1, y1 being Element of Day A st
( a = [x1,y1] & (born x1) (+) (born y1) c= A ) ;
hence a in [:(Day A),(Day A):] by ZFMISC_1:87; :: thesis: verum

end;

then reconsider IT = { [x,y] where x, y is Element of Day A : (born x) (+) (born y) c= A } as Subset of [:(Day A),(Day A):] ;
take IT ; :: thesis: for x, y being Surreal holds
( [x,y] in IT iff (born x) (+) (born y) c= A )
let x, y be Surreal; :: thesis: ( [x,y] in IT iff (born x) (+) (born y) c= A )
thus ( [x,y] in IT implies (born x) (+) (born y) c= A ) :: thesis: ( (born x) (+) (born y) c= A implies [x,y] in IT )

proof

assume [x,y] in IT ; :: thesis: (born x) (+) (born y) c= A
then consider x1, y1 being Element of Day A such that
A1: ( [x,y] = [x1,y1] & (born x1) (+) (born y1) c= A ) ;
( x = x1 & y = y1 ) by A1, XTUPLE_0:1;
hence (born x) (+) (born y) c= A by A1; :: thesis: verum

end;

A2: ( born x c= (born x) (+) (born y) & born y c= (born x) (+) (born y) ) by ORDINAL7:86;
assume A3: (born x) (+) (born y) c= A ; :: thesis: [x,y] in IT
then ( born x c= A & born y c= A ) by A2, XBOOLE_1:1;
then ( x in Day (born x) & Day (born x) c= Day A & y in Day (born y) & Day (born y) c= Day A ) by SURREAL0:35, SURREAL0:def 18;
hence [x,y] in IT by A3; :: thesis: verum