let x, y be Surreal; :: thesis:
let X1, X2, Y1, Y2 be set ; :: thesis:
assume A1: ( X1 <==> X2 & Y1 <==> Y2 & x = [X1,Y1] & y = [X2,Y2] ) ; :: thesis:

A2: now :: thesis:

let x be Surreal; :: thesis:
assume x in X1 ; :: thesis:
then ex y1, y2 being Surreal st
( y1 in X2 & y2 in X2 & y1 <= x & x <= y2 ) by A1, Def3;
hence ex y being Surreal st
( y in X2 & x <= y ) ; :: thesis:

end;

A3: now :: thesis:

let x be Surreal; :: thesis:
assume x in Y2 ; :: thesis:
then ex y1, y2 being Surreal st
( y1 in Y1 & y2 in Y1 & y1 <= x & x <= y2 ) by A1, Def3;
hence ex y being Surreal st
( y in Y1 & y <= x ) ; :: thesis:

end;

A4: now :: thesis:

let x be Surreal; :: thesis:
assume x in X2 ; :: thesis:
then ex y1, y2 being Surreal st
( y1 in X1 & y2 in X1 & y1 <= x & x <= y2 ) by A1, Def3;
hence ex y being Surreal st
( y in X1 & x <= y ) ; :: thesis:

end;

let x be Surreal; :: thesis:
assume x in Y1 ; :: thesis:
then ex y1, y2 being Surreal st
( y1 in Y2 & y2 in Y2 & y1 <= x & x <= y2 ) by A1, Def3;
hence ex y being Surreal st
( y in Y2 & y <= x ) ; :: thesis:

end;

hence x == y by SURREAL0:44, A1, A2, A3, A4; :: thesis: