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

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

then inf X in X by XXREAL_2:def 5;
hence inf X is ext-natural ; :: thesis: verum

end;

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

hence inf X is ext-natural by XXREAL_2:38; :: thesis: verum

end;

end;