let C1, C2 be surreal-membered set ; :: thesis: ( ( for o being object holds
( o in C1 iff ( o is surreal & (L_ o) \/ (R_ o) c= A ) ) ) & ( for o being object holds
( o in C2 iff ( o is surreal & (L_ o) \/ (R_ o) c= A ) ) ) implies C1 = C2 )
assume that
A6: for o being object holds
( o in C1 iff ( o is surreal & (L_ o) \/ (R_ o) c= A ) ) and
A7: for o being object holds
( o in C2 iff ( o is surreal & (L_ o) \/ (R_ o) c= A ) ) ; :: thesis: C1 = C2

now :: thesis: for x being object holds
( x in C1 iff x in C2 )

let x be object ; :: thesis: ( x in C1 iff x in C2 )
( x in C1 iff ( x is surreal & (L_ x) \/ (R_ x) c= A ) ) by A6;
hence ( x in C1 iff x in C2 ) by A7; :: thesis: verum

end;

hence C1 = C2 by TARSKI:2; :: thesis: verum