let x be object ; :: thesis:
assume x in X \/ Y ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose x in X ; :: thesis:

hence x is ext-natural ; :: thesis:

end;

suppose x in Y ; :: thesis:

hence x is ext-natural ; :: thesis:

end;

end;

end;

hence X \/ Y is ext-natural-membered ; :: thesis: