let L be complete LATTICE; :: thesis: for A being Subset of L st A is lower holds
( A ` in xi L iff A is closed_under_directed_sups )
let A be Subset of L; :: thesis: ( A is lower implies ( A ` in xi L iff A is closed_under_directed_sups ) )
assume A1: A is lower ; :: thesis: ( A ` in xi L iff A is closed_under_directed_sups )
then reconsider A1 = A as lower Subset of L ;
A2: A1 ` is upper ;
consider T being Scott TopAugmentation of L;
A3: RelStr(# the carrier of L,the InternalRel of L #) = RelStr(# the carrier of T,the InternalRel of T #) by YELLOW_9:def 4;
then reconsider A' = A as Subset of T ;
reconsider A' = A' as Subset of T ;
thus ( A ` in xi L implies A is closed_under_directed_sups ) :: thesis: ( A is closed_under_directed_sups implies A ` in xi L )

proof

assume A ` in xi L ; :: thesis: A is closed_under_directed_sups
then A' ` in sigma L by A2, A3, Th30;
then A' ` in the topology of T by YELLOW_9:51;
then A' ` is open by PRE_TOPC:def 5;
then A' is closed by TOPS_1:29;
then A' is closed_under_directed_sups by WAYBEL11:7;
hence A is closed_under_directed_sups by A3, YELLOW12:20; :: thesis: verum

end;

assume A is closed_under_directed_sups ; :: thesis: A ` in xi L
then A4: A' is closed_under_directed_sups by A3, YELLOW12:20;
A' is lower by A1, A3, WAYBEL_0:25;
then A' is closed by A4, WAYBEL11:7;
then A' ` is open by TOPS_1:29;
then A' ` in the topology of T by PRE_TOPC:def 5;
then A ` in sigma L by A3, YELLOW_9:51;
hence A ` in xi L by Th29; :: thesis: verum