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 ) )

set T = the Scott TopAugmentation of L;

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: RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of the Scott TopAugmentation of L, the InternalRel of the Scott TopAugmentation of L #) by YELLOW_9:def 4;

then reconsider A9 = A as Subset of the Scott TopAugmentation of L ;

reconsider A9 = A9 as Subset of the Scott TopAugmentation of L ;

A3: A1 ` is upper ;

thus ( A ` in xi L implies A is closed_under_directed_sups ) :: thesis: ( A is closed_under_directed_sups implies A ` in xi L )

then A4: A9 is directly_closed by A2, YELLOW12:20;

A9 is lower by A1, A2, WAYBEL_0:25;

then A9 is closed by A4, WAYBEL11:7;

then A9 ` is open by TOPS_1:3;

then A9 ` in the topology of the Scott TopAugmentation of L by PRE_TOPC:def 2;

then A ` in sigma L by A2, YELLOW_9:51;

hence A ` in xi L by Th28; :: thesis: verum

( 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 ) )

set T = the Scott TopAugmentation of L;

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: RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of the Scott TopAugmentation of L, the InternalRel of the Scott TopAugmentation of L #) by YELLOW_9:def 4;

then reconsider A9 = A as Subset of the Scott TopAugmentation of L ;

reconsider A9 = A9 as Subset of the Scott TopAugmentation of L ;

A3: A1 ` is upper ;

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 is closed_under_directed_sups
; :: thesis: A ` in xi L
assume
A ` in xi L
; :: thesis: A is closed_under_directed_sups

then A9 ` in sigma L by A3, A2, Th29;

then A9 ` in the topology of the Scott TopAugmentation of L by YELLOW_9:51;

then A9 ` is open by PRE_TOPC:def 2;

then A9 is closed by TOPS_1:3;

then A9 is directly_closed by WAYBEL11:7;

hence A is closed_under_directed_sups by A2, YELLOW12:20; :: thesis: verum

end;then A9 ` in sigma L by A3, A2, Th29;

then A9 ` in the topology of the Scott TopAugmentation of L by YELLOW_9:51;

then A9 ` is open by PRE_TOPC:def 2;

then A9 is closed by TOPS_1:3;

then A9 is directly_closed by WAYBEL11:7;

hence A is closed_under_directed_sups by A2, YELLOW12:20; :: thesis: verum

then A4: A9 is directly_closed by A2, YELLOW12:20;

A9 is lower by A1, A2, WAYBEL_0:25;

then A9 is closed by A4, WAYBEL11:7;

then A9 ` is open by TOPS_1:3;

then A9 ` in the topology of the Scott TopAugmentation of L by PRE_TOPC:def 2;

then A ` in sigma L by A2, YELLOW_9:51;

hence A ` in xi L by Th28; :: thesis: verum