for x being ExtReal st x in X holds
0 <= x ;
then reconsider L = 0 as LowerBound of X by XXREAL_2:def 2;
take L ; :: thesis: L is ext-natural
thus L is ext-natural ; :: thesis: verum