let L be non empty Poset; :: thesis: for x being Element of L holds

( ex_sup_of downarrow x,L & sup (downarrow x) = x )

let x be Element of L; :: thesis: ( ex_sup_of downarrow x,L & sup (downarrow x) = x )

ex_sup_of {x},L by YELLOW_0:38;

hence ex_sup_of downarrow x,L by Th32; :: thesis: sup (downarrow x) = x

thus sup (downarrow x) = sup {x} by Th33, YELLOW_0:38

.= x by YELLOW_0:39 ; :: thesis: verum

( ex_sup_of downarrow x,L & sup (downarrow x) = x )

let x be Element of L; :: thesis: ( ex_sup_of downarrow x,L & sup (downarrow x) = x )

ex_sup_of {x},L by YELLOW_0:38;

hence ex_sup_of downarrow x,L by Th32; :: thesis: sup (downarrow x) = x

thus sup (downarrow x) = sup {x} by Th33, YELLOW_0:38

.= x by YELLOW_0:39 ; :: thesis: verum