let T be complete Lawson TopLattice; :: thesis:
consider S being Scott TopAugmentation of T;
let F be non empty filtered Subset of T; :: thesis:
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;
A3: the topology of S = sigma T by YELLOW_9:51;
A4: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) by YELLOW_9:def 4;
thus Lim (F opp+id ) c= {(inf F)} :: according to XBOOLE_0:def 10 :: thesis:

let p be set ; :: according to TARSKI:def 3 :: thesis:
assume A5: p in Lim (F opp+id ) ; :: thesis:
then reconsider p = p as Element of T ;
p is_<=_than F

let u be Element of T; :: according to LATTICE3:def 8 :: thesis:
assume A6: u in F ; :: thesis:
downarrow u is closed by Th38;
then A7: Cl (downarrow u) = downarrow u by PRE_TOPC:52;
F opp+id is_eventually_in downarrow u

reconsider i = u as Element of (F opp+id ) by A6, YELLOW_9:7;
take i ; :: according to WAYBEL_0:def 11 :: thesis:
let j be Element of (F opp+id ); :: thesis:
j in F by A1;
then reconsider z = j as Element of T ;
assume j >= i ; :: thesis:
then z ~ >= u ~ by A2, YELLOW_0:60;
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:

end;

then Lim (F opp+id ) c= downarrow u by A7, Th26;
hence p <= u by A5, WAYBEL_0:17; :: thesis:

end;

then A8: p <= inf F by YELLOW_0:33;
inf F is_<=_than F by YELLOW_0:33;
then A9: 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:52;
then A10: Cl F c= uparrow (inf F) by A9, PRE_TOPC:49;
the mapping of (F opp+id ) = id F by Th27;
then rng the mapping of (F opp+id ) = F by RELAT_1:71;
then p in Cl F by A5, WAYBEL_9:24;
then p >= inf F by A10, WAYBEL_0:18;
then p = inf F by A8, ORDERS_2:25;
hence p in {(inf F)} by TARSKI:def 1; :: thesis:

end;

reconsider K = (sigma T) \/ { ((uparrow x) ` ) where x is Element of T : verum } as prebasis of T by Th30;

let A be Subset of T; :: thesis:
assume A11: ( inf F in A & A in K ) ; :: thesis:

per cases by A11, XBOOLE_0:def 3;

suppose A12: A in sigma T ; :: thesis:

then reconsider a = A as Subset of S by A3;
a is open by A3, A12, PRE_TOPC:def 5;
then a is upper by WAYBEL11:def 4;
then A13: A is upper by A4, WAYBEL_0:25;
consider i being Element of (F opp+id );
thus F opp+id is_eventually_in A :: thesis:

take i ; :: according to WAYBEL_0:def 11 :: thesis:
let j be Element of (F opp+id ); :: thesis:
j in F by A1;
then reconsider z = j as Element of T ;
z >= inf F by A1, YELLOW_2:24;
then z in A by A11, A13, WAYBEL_0:def 20;
hence ( not i <= j or (F opp+id ) . j in A ) by YELLOW_9:7; :: thesis:

end;

suppose A in { ((uparrow x) ` ) where x is Element of T : verum } ; :: thesis:

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

reconsider i = y as Element of (F opp+id ) by A15, YELLOW_9:7;
take i ; :: according to WAYBEL_0:def 11 :: thesis:
let j be Element of (F opp+id ); :: thesis:
j in F by A1;
then reconsider z = j as Element of T ;
assume j >= i ; :: thesis:
then z ~ >= y ~ by A2, YELLOW_0:60;
then z <= y by LATTICE3:9;
then not z >= x by A15, ORDERS_2:26;
then z in A by A14, YELLOW_9:1;
hence (F opp+id ) . j in A by YELLOW_9:7; :: thesis:

end;

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