now :: thesis: for x being object st x in X /\ Y holds
x is ext-natural

let x be object ; :: thesis: ( x in X /\ Y implies x is ext-natural )
assume x in X /\ Y ; :: thesis: x is ext-natural
then x in X by XBOOLE_0:def 4;
hence x is ext-natural ; :: thesis: verum

end;

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