let x be Element of X; :: thesis: x is ext-natural

per cases ( not X is empty or X is empty ) ;

suppose not X is empty ; :: thesis: x is ext-natural

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

end;

suppose X is empty ; :: thesis: x is ext-natural

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

end;

end;