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 )
assume A1: A is upper ; :: thesis: ( not A in xi L or A in sigma L )
assume A2: A in xi L ; :: thesis: A in sigma L
consider T being Scott TopAugmentation of L;
A3: RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of L,the InternalRel of L #) by YELLOW_9:def 4;
then reconsider A' = A as Subset of T ;
reconsider A' = A' as Subset of T ;
A4: A' is property(S) by A2, A3, Th28, YELLOW12:19;
A' is upper by A1, A3, WAYBEL_0:25;
then A' is open by A4, WAYBEL11:15;
then A' in the topology of T by PRE_TOPC:def 5;
hence A in sigma L by YELLOW_9:51; :: thesis: verum