let L be ExtReal; :: thesis: ( L is LowerBound of X iff for N being ExtNat st N in X holds
L <= N )
thus ( L is LowerBound of X implies for N being ExtNat st N in X holds
L <= N ) by XXREAL_2:def 2; :: thesis: ( ( for N being ExtNat st N in X holds
L <= N ) implies L is LowerBound of X )
assume for N being ExtNat st N in X holds
L <= N ; :: thesis: L is LowerBound of X
then for x being ExtReal st x in X holds
L <= x ;
hence L is LowerBound of X by XXREAL_2:def 2; :: thesis: verum