let T be complete Lawson TopLattice; :: thesis: for A being lower Subset of T holds
( A is closed iff A is closed_under_directed_sups )
let A be lower Subset of T; :: thesis: ( A is closed iff A is closed_under_directed_sups )

hereby :: thesis: ( A is closed_under_directed_sups implies A is closed )

assume A is closed ; :: thesis: A is closed_under_directed_sups
then A ` is open by TOPS_1:29;
then reconsider mA = A ` as property(S) Subset of T by Th36;
mA ` = A ;
hence A is closed_under_directed_sups ; :: thesis: verum

end;

assume A is closed_under_directed_sups ; :: thesis: A is closed
then reconsider dA = A as lower directly_closed Subset of T ;
consider S being Scott TopAugmentation of T;
A1: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) by YELLOW_9:def 4;
then reconsider mA = dA ` as Subset of S ;
( mA is upper & mA is inaccessible_by_directed_joins ) by A1, WAYBEL_0:25, YELLOW_9:47;
then ( mA is open & T is TopAugmentation of S ) by A1, WAYBEL11:def 4, YELLOW_9:def 4;
then dA ` is open by Th37;
hence A is closed by TOPS_1:29; :: thesis: verum