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 or o in Y ) by XBOOLE_0:def 3;
hence o is surreal by Def16; :: thesis: verum