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

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