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 b₁ is ext-natural )
assume x in X \/ Y ; :: thesis: b₁ is ext-natural

per cases then ( x in X or x in Y ) by XBOOLE_0:def 3;

suppose x in X ; :: thesis: b₁ is ext-natural

hence x is ext-natural ; :: thesis: verum

end;

suppose x in Y ; :: thesis: b₁ is ext-natural

hence x is ext-natural ; :: thesis: verum

end;

end;

end;

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