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 A1: ( 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 ) ) ; :: 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 & a2 = a ) by A1;
hence contradiction by A2; :: thesis: verum