let o be object ; :: according to SURREAL0:def 16 :: thesis: ( o in X /\ Y implies o is surreal )
assume o in X /\ Y ; :: thesis: o is surreal
then o in X by XBOOLE_0:def 4;
hence o is surreal by Def16; :: thesis: verum