let L be Chain; :: thesis: ( L is up-complete & L is lower-bounded implies L is complete )
assume A1: ( L is up-complete & L is lower-bounded ) ; :: thesis: L is complete

now :: thesis: for X being Subset of L holds ex_sup_of X,L

let X be Subset of L; :: thesis: ex_sup_of X,L
( X = {} or X <> {} ) ;
hence ex_sup_of X,L by A1, WAYBEL_0:75, YELLOW_0:42; :: thesis: verum

end;

hence L is complete by YELLOW_0:53; :: thesis: verum