( ex_sup_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 Def7;
hence ( ex_sup_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
b₁ <= a ) ) ) ; :: thesis: verum