let o be object ; :: according to SURREALO:def 12 :: thesis: ( o in X \/ Y implies o is uSurreal )
assume o in X \/ Y ; :: thesis: o is uSurreal
then ( o in X or o in Y ) by XBOOLE_0:def 3;
hence o is uSurreal by Def12; :: thesis: verum