defpred S₁[ object ] means $1 is surreal ;
consider X being set such that
A1: for x being object holds
( x in X iff ( x in [:(bool A),(bool A):] & S₁[x] ) ) from XBOOLE_0:sch 1();
X is surreal-membered by A1;
then reconsider X = X as surreal-membered set ;
take X ; :: thesis: for o being object holds
( o in X iff ( o is surreal & (L_ o) \/ (R_ o) c= A ) )
let o be object ; :: thesis: ( o in X iff ( o is surreal & (L_ o) \/ (R_ o) c= A ) )
thus ( o in X implies ( o is surreal & (L_ o) \/ (R_ o) c= A ) ) :: thesis: ( o is surreal & (L_ o) \/ (R_ o) c= A implies o in X )

proof

assume A2: o in X ; :: thesis: ( o is surreal & (L_ o) \/ (R_ o) c= A )
then ( o in [:(bool A),(bool A):] & S₁[o] ) by A1;
then consider a, b being object such that
A3: ( a in bool A & b in bool A & o = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as set by TARSKI:1;
thus ( o is surreal & (L_ o) \/ (R_ o) c= A ) by A1, A2, A3, XBOOLE_1:8; :: thesis: verum

end;

assume A4: ( o is surreal & (L_ o) \/ (R_ o) c= A ) ; :: thesis: o in X
then reconsider O = o as Surreal ;
A5: O = [(L_ o),(R_ o)] ;
( L_ o c= (L_ o) \/ (R_ o) & R_ o c= (L_ o) \/ (R_ o) ) by XBOOLE_1:7;
then ( L_ o c= A & R_ o c= A ) by A4, XBOOLE_1:1;
then o in [:(bool A),(bool A):] by A5, ZFMISC_1:def 2;
hence o in X by A4, A1; :: thesis: verum