( ex_inf_of X,L implies ex a being Element of L st
( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds
b <= a ) & ( for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds
b <= c ) holds
c = a ) ) ) by Def8;
hence ( ex_inf_of X,L implies ex b₁ being Element of L st
( X is_>=_than b₁ & ( for a being Element of L st X is_>=_than a holds
a <= b₁ ) ) ) ; :: thesis: verum