let a1, a2 be Element of L; :: thesis: ( ex_sup_of X,L & X is_<=_than a1 & ( for a being Element of L st X is_<=_than a holds
a1 <= a ) & X is_<=_than a2 & ( for a being Element of L st X is_<=_than a holds
a2 <= a ) implies a1 = a2 )
given a being Element of L such that X is_<=_than a and
for b being Element of L st X is_<=_than b holds
b >= a and
A1: 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 ; :: according to YELLOW_0:def 7 :: thesis: ( not X is_<=_than a1 or ex a being Element of L st
( X is_<=_than a & not a1 <= a ) or not X is_<=_than a2 or ex a being Element of L st
( X is_<=_than a & not a2 <= a ) or a1 = a2 )
assume A2: ( X is_<=_than a1 & ( for a being Element of L st X is_<=_than a holds
a1 <= a ) & X is_<=_than a2 & ( for a being Element of L st X is_<=_than a holds
a2 <= a ) & not a1 = a2 ) ; :: thesis: contradiction
then a1 = a by A1;
hence contradiction by A1, A2; :: thesis: verum