let T be complete Lawson TopLattice; :: thesis: for F being non empty filtered Subset of T holds Lim (F opp+id) = {(inf F)}
reconsider K = (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } as prebasis of T by Th30;
set S = the Scott TopAugmentation of T;
let F be non empty filtered Subset of T; :: thesis: Lim (F opp+id) = {(inf F)}
set N = F opp+id ;
A1: the carrier of (F opp+id) = F by YELLOW_9:7;
A2: F opp+id is full SubRelStr of T opp by YELLOW_9:7;
thus Lim (F opp+id) c= {(inf F)} :: according to XBOOLE_0:def 10 :: thesis: {(inf F)} c= Lim (F opp+id)

proof

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in Lim (F opp+id) or p in {(inf F)} )
assume A3: p in Lim (F opp+id) ; :: thesis: p in {(inf F)}
then reconsider p = p as Element of T ;
the mapping of (F opp+id) = id F by Th27;
then rng the mapping of (F opp+id) = F by RELAT_1:45;
then A4: p in Cl F by A3, WAYBEL_9:24;
p is_<=_than F

proof

let u be Element of T; :: according to LATTICE3:def 8 :: thesis: ( not u in F or p <= u )
assume A5: u in F ; :: thesis: p <= u
A6: F opp+id is_eventually_in downarrow u

proof

reconsider i = u as Element of (F opp+id) by A5, YELLOW_9:7;
take i ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of (F opp+id) holds
( not i <= b₁ or (F opp+id) . b₁ in downarrow u )
let j be Element of (F opp+id); :: thesis: ( not i <= j or (F opp+id) . j in downarrow u )
j in F by A1;
then reconsider z = j as Element of T ;
assume j >= i ; :: thesis: (F opp+id) . j in downarrow u
then z ~ >= u ~ by A2, YELLOW_0:59;
then z <= u by LATTICE3:9;
then z in downarrow u by WAYBEL_0:17;
hence (F opp+id) . j in downarrow u by YELLOW_9:7; :: thesis: verum

end;

downarrow u is closed by Th38;
then Cl (downarrow u) = downarrow u by PRE_TOPC:22;
then Lim (F opp+id) c= downarrow u by A6, Th26;
hence p <= u by A3, WAYBEL_0:17; :: thesis: verum

end;

then A7: p <= inf F by YELLOW_0:33;
inf F is_<=_than F by YELLOW_0:33;
then A8: F c= uparrow (inf F) by YELLOW_2:2;
uparrow (inf F) is closed by Th38;
then Cl (uparrow (inf F)) = uparrow (inf F) by PRE_TOPC:22;
then Cl F c= uparrow (inf F) by A8, PRE_TOPC:19;
then p >= inf F by A4, WAYBEL_0:18;
then p = inf F by A7, ORDERS_2:2;
hence p in {(inf F)} by TARSKI:def 1; :: thesis: verum

end;

A9: the topology of the Scott TopAugmentation of T = sigma T by YELLOW_9:51;
A10: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def 4;

now :: thesis: for A being Subset of T st inf F in A & A in K holds
F opp+id is_eventually_in A

let A be Subset of T; :: thesis: ( inf F in A & A in K implies F opp+id is_eventually_in b₁ )
assume that
A11: inf F in A and
A12: A in K ; :: thesis: F opp+id is_eventually_in b₁

per cases ( A in sigma T or A in { ((uparrow x) `) where x is Element of T : verum } ) by A12, XBOOLE_0:def 3;

suppose A13: A in sigma T ; :: thesis: F opp+id is_eventually_in b₁

then reconsider a = A as Subset of the Scott TopAugmentation of T by A9;
set i = the Element of (F opp+id);
a is open by A9, A13;
then a is upper by WAYBEL11:def 4;
then A14: A is upper by A10, WAYBEL_0:25;
thus F opp+id is_eventually_in A :: thesis: verum

proof

take the Element of (F opp+id) ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of (F opp+id) holds
( not the Element of (F opp+id) <= b₁ or (F opp+id) . b₁ in A )
let j be Element of (F opp+id); :: thesis: ( not the Element of (F opp+id) <= j or (F opp+id) . j in A )
j in F by A1;
then reconsider z = j as Element of T ;
z >= inf F by A1, YELLOW_2:22;
then z in A by A11, A14;
hence ( not the Element of (F opp+id) <= j or (F opp+id) . j in A ) by YELLOW_9:7; :: thesis: verum

end;

end;

suppose A in { ((uparrow x) `) where x is Element of T : verum } ; :: thesis: F opp+id is_eventually_in b₁

then consider x being Element of T such that
A15: A = (uparrow x) ` ;
not inf F >= x by A11, A15, YELLOW_9:1;
then not F is_>=_than x by YELLOW_0:33;
then consider y being Element of T such that
A16: y in F and
A17: not y >= x ;
thus F opp+id is_eventually_in A :: thesis: verum

proof

reconsider i = y as Element of (F opp+id) by A16, YELLOW_9:7;
take i ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of (F opp+id) holds
( not i <= b₁ or (F opp+id) . b₁ in A )
let j be Element of (F opp+id); :: thesis: ( not i <= j or (F opp+id) . j in A )
j in F by A1;
then reconsider z = j as Element of T ;
assume j >= i ; :: thesis: (F opp+id) . j in A
then z ~ >= y ~ by A2, YELLOW_0:59;
then z <= y by LATTICE3:9;
then not z >= x by A17, ORDERS_2:3;
then z in A by A15, YELLOW_9:1;
hence (F opp+id) . j in A by YELLOW_9:7; :: thesis: verum

end;

end;

end;

end;

then inf F in Lim (F opp+id) by Th25;
hence {(inf F)} c= Lim (F opp+id) by ZFMISC_1:31; :: thesis: verum