let T be non empty reflexive transitive up-complete Scott TopRelStr ; :: thesis: for S being Subset of T holds
( S is closed iff ( S is directly_closed & S is lower ) )
let S be Subset of T; :: thesis: ( S is closed iff ( S is directly_closed & S is lower ) )

hereby :: thesis: ( S is directly_closed & S is lower implies S is closed )

assume S is closed ; :: thesis: ( S is directly_closed & S is lower )
then S ` is open ;
then reconsider A = S ` as upper inaccessible Subset of T by Def4;
( A ` is directly_closed & A ` is lower ) ;
hence ( S is directly_closed & S is lower ) ; :: thesis: verum

end;

assume ( S is directly_closed & S is lower ) ; :: thesis: S is closed
then reconsider S = S as lower directly_closed Subset of T ;
S ` is open by Def4;
hence S is closed ; :: thesis: verum