let T be up-complete LATTICE; :: thesis: for x being Element of T holds downarrow x is directly_closed
let x be Element of T; :: thesis: downarrow x is directly_closed
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 by A1, WAYBEL_0:17;
then sup D <= x by A2, YELLOW_0:30;
hence "\/" (D,T) in downarrow x by WAYBEL_0:17; :: thesis: verum