let T be up-complete LATTICE; :: thesis: for x being Element of T holds downarrow x is closed_under_directed_sups
let x be Element of T; :: thesis: downarrow x is closed_under_directed_sups
let D be non empty directed Subset of T; :: according to WAYBEL11:def 2 :: thesis: ( not D c= downarrow x or "\/" D,T in downarrow x )
assume A1: D c= downarrow x ; :: thesis: "\/" D,T in downarrow x
A2: ex_sup_of D,T by WAYBEL_0:75;
x is_>=_than D

proof

let b be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not b in D or b <= x )
assume b in D ; :: thesis: b <= x
hence b <= x by A1, WAYBEL_0:17; :: thesis: verum

end;

then sup D <= x by A2, YELLOW_0:30;
hence "\/" D,T in downarrow x by WAYBEL_0:17; :: thesis: verum