let T be non empty reflexive transitive antisymmetric up-complete TopRelStr ; :: 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
downarrow x is directly_closed
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def 2 :: thesis: ( D c= downarrow x implies sup D in downarrow x )
assume A1: D c= downarrow x ; :: thesis: sup D in downarrow x
ex a being Element of T st
( a is_>=_than D & ( for b being Element of T st b is_>=_than D holds
a <= b ) ) by WAYBEL_0:def 39;
then A2: ex_sup_of D,T by YELLOW_0:15;
x is_>=_than D by A1, WAYBEL_0:17;
then sup D <= x by A2, YELLOW_0:30;
hence sup D in downarrow x by WAYBEL_0:17; :: thesis: verum
end;
hence downarrow x is directly_closed ; :: thesis: verum