let a1, a2 be Element of L; :: thesis: ( ex_inf_of X,L & X is_>=_than a1 & ( for a being Element of L st X is_>=_than a holds
a <= a1 ) & X is_>=_than a2 & ( for a being Element of L st X is_>=_than a holds
a <= a2 ) 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
A3: 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 8 :: thesis: ( not X is_>=_than a1 or ex a being Element of L st
( X is_>=_than a & not a <= a1 ) or not X is_>=_than a2 or ex a being Element of L st
( X is_>=_than a & not a <= a2 ) or a1 = a2 )
assume A4: ( X is_>=_than a1 & ( for a being Element of L st X is_>=_than a holds
a <= a1 ) & X is_>=_than a2 & ( for a being Element of L st X is_>=_than a holds
a <= a2 ) & not a1 = a2 ) ; :: thesis: contradiction
then a1 = a by A3;
hence contradiction by A3, A4; :: thesis: verum