let L be antisymmetric RelStr ; :: thesis: for X being set holds
( ex_sup_of X,L iff ex a being Element of L st
( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds
a <= b ) ) )
let X be set ; :: thesis: ( ex_sup_of X,L iff ex a being Element of L st
( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds
a <= b ) ) )

hereby :: thesis: ( ex a being Element of L st
( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds
a <= b ) ) implies ex_sup_of X,L )

assume ex_sup_of X,L ; :: thesis: ex a being Element of L st
( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds
a <= b ) )
then 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 a being Element of L st
( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds
a <= b ) ) ; :: thesis: verum

end;

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
a <= b ) ) ; :: thesis: ex_sup_of X,L
take a ; :: according to YELLOW_0:def 7 :: thesis: ( 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 ) )
thus ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds
b >= a ) ) by A1; :: thesis: 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
let c be Element of L; :: thesis: ( X is_<=_than c & ( for b being Element of L st X is_<=_than b holds
b >= c ) implies c = a )
assume ( X is_<=_than c & ( for b being Element of L st X is_<=_than b holds
b >= c ) ) ; :: thesis: c = a
then ( a <= c & c <= a ) by A1;
hence c = a by ORDERS_2:2; :: thesis: verum