let L be antisymmetric RelStr ; :: thesis: for a being Element of L
for X being set holds
( a = "\/" (X,L) & ex_sup_of X,L iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds
a <= b ) ) )
let a be Element of L; :: thesis: for X being set holds
( a = "\/" (X,L) & ex_sup_of X,L iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds
a <= b ) ) )
let X be set ; :: thesis: ( a = "\/" (X,L) & ex_sup_of X,L iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds
a <= b ) ) )
( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds
a <= b ) implies ex_sup_of X,L ) by Th15;
hence ( a = "\/" (X,L) & ex_sup_of X,L iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds
a <= b ) ) ) by Def9; :: thesis: verum