let L be complete LATTICE; :: thesis: for A being Subset of L st A is upper & A in xi L holds

A in sigma L

let A be Subset of L; :: thesis: ( A is upper & A in xi L implies A in sigma L )

set T = the Scott TopAugmentation of L;

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

assume A is upper ; :: thesis: ( not A in xi L or A in sigma L )

then A2: A9 is upper by A1, WAYBEL_0:25;

assume A in xi L ; :: thesis: A in sigma L

then A9 is property(S) by A1, Th27, YELLOW12:19;

then A9 is open by A2, WAYBEL11:15;

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

hence A in sigma L by YELLOW_9:51; :: thesis: verum

A in sigma L

let A be Subset of L; :: thesis: ( A is upper & A in xi L implies A in sigma L )

set T = the Scott TopAugmentation of L;

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

assume A is upper ; :: thesis: ( not A in xi L or A in sigma L )

then A2: A9 is upper by A1, WAYBEL_0:25;

assume A in xi L ; :: thesis: A in sigma L

then A9 is property(S) by A1, Th27, YELLOW12:19;

then A9 is open by A2, WAYBEL11:15;

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

hence A in sigma L by YELLOW_9:51; :: thesis: verum