let IT1, IT2 be surreal-membered set ; :: thesis: ( ( for y being Surreal holds
( y in IT1 iff ( y == x & y in Day (born_eq x) ) ) ) & ( for y being Surreal holds
( y in IT2 iff ( y == x & y in Day (born_eq x) ) ) ) implies IT1 = IT2 )
assume that
A3: for y being Surreal holds
( y in IT1 iff ( y == x & y in Day (born_eq x) ) ) and
A4: for y being Surreal holds
( y in IT2 iff ( y == x & y in Day (born_eq x) ) ) ; :: thesis: IT1 = IT2
thus IT1 c= IT2 :: according to XBOOLE_0:def 10 :: thesis: IT2 c= IT1

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in IT1 or o in IT2 )
assume A5: o in IT1 ; :: thesis: o in IT2
then reconsider o = o as Surreal by SURREAL0:def 16;
( o == x & o in Day (born_eq x) ) by A3, A5;
hence o in IT2 by A4; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in IT2 or o in IT1 )
assume A6: o in IT2 ; :: thesis: o in IT1
then reconsider o = o as Surreal by SURREAL0:def 16;
( o == x & o in Day (born_eq x) ) by A4, A6;
hence o in IT1 by A3; :: thesis: verum