let L be lower-bounded continuous LATTICE; :: thesis:
let V be upper Open Subset of L; :: thesis:
let F be Filter of L; :: thesis:
let v be Element of L; :: thesis:
assume that
A1: V "/\" F c= V and
A2: v in V ; :: thesis:
reconsider V1 = V as non empty upper Open Subset of L by A2;
reconsider v1 = v as Element of V1 by A2;
reconsider G = { x where x is Element of L : V "/\" {x} c= V } as Filter of L by Th23, Th24, Th25;
given A being non empty GeneratorSet of F such that A3: A is countable ; :: thesis:
consider f being sequence of A such that
A4: rng f = A by A3, CARD_3:96;
reconsider f = f as sequence of the carrier of L by FUNCT_2:7;
deffunc H₁( Element of NAT ) -> Element of the carrier of L = "/\" ( { (f . m) where m is Element of NAT : m <= $1 } ,L);
consider g being sequence of the carrier of L such that
A5: for n being Element of NAT holds g . n = H₁(n) from FUNCT_2:sch 4();
defpred S₁[ Nat, set , set ] means ex x1, y1 being Element of V1 ex z1 being Element of L st
( x1 = $2 & y1 = $3 & z1 = g . ($1 + 1) & y1 << x1 "/\" z1 );
A6: dom g = NAT by FUNCT_2:def 1;
then reconsider AA = rng g as non empty Subset of L by RELAT_1:42;
A7: AA is GeneratorSet of F by A4, A5, Th32;
A8: F c= G

proof

let q be object ; :: according to TARSKI:def 3 :: thesis:
assume A9: q in F ; :: thesis:
then reconsider s = q as Element of L ;
A10: V "/\" {s} = { (s "/\" t) where t is Element of L : t in V } by YELLOW_4:42;
V "/\" {s} c= V

proof

let w be object ; :: according to TARSKI:def 3 :: thesis:
assume w in V "/\" {s} ; :: thesis:
then consider t being Element of L such that
A11: w = s "/\" t and
A12: t in V by A10;
t "/\" s in V "/\" F by A9, A12;
hence w in V by A1, A11; :: thesis:

end;

hence q in G ; :: thesis:

end;

A13: for n being Nat
for x being Element of V1 ex y being Element of V1 st S₁[n,x,y]

proof

let n be Nat; :: thesis:
let x be Element of V1; :: thesis:
AA c= F by A7, Lm4;
then A14: AA c= G by A8;
g . (n + 1) in AA by A6, FUNCT_1:def 3;
then g . (n + 1) in G by A14;
then consider g1 being Element of L such that
A15: g . (n + 1) = g1 and
A16: V "/\" {g1} c= V ;
g1 in {g1} by TARSKI:def 1;
then x "/\" g1 in V "/\" {g1} ;
then ex y1 being Element of L st
( y1 in V & y1 << x "/\" g1 ) by A16, WAYBEL_6:def 1;
hence ex y being Element of V1 st S₁[n,x,y] by A15; :: thesis:

end;

consider h being sequence of V1 such that
A17: h . 0 = v1 and
A18: for n being Nat holds S₁[n,h . n,h . (n + 1)] from RECDEF_1:sch 2(A13);
A19: dom h = NAT by FUNCT_2:def 1;
then A20: h . 0 in rng h by FUNCT_1:def 3;
then reconsider R = rng h as non empty Subset of L by XBOOLE_1:1;
set O = uparrow (fininfs R);
A21: R c= uparrow (fininfs R) by WAYBEL_0:62;
A22: for x, y being Element of L
for n being Nat st h . n = x & h . (n + 1) = y holds
y <= x

proof

let x, y be Element of L; :: thesis:
let n be Nat; :: thesis:
assume A23: ( h . n = x & h . (n + 1) = y ) ; :: thesis:
consider x1, y1 being Element of V1, z1 being Element of L such that
A24: ( x1 = h . n & y1 = h . (n + 1) ) and
z1 = g . (n + 1) and
A25: y1 << x1 "/\" z1 by A18;
A26: x1 "/\" z1 <= x1 by YELLOW_0:23;
y1 <= x1 "/\" z1 by A25, WAYBEL_3:1;
hence y <= x by A23, A24, A26, ORDERS_2:3; :: thesis:

end;

A27: for x, y being Element of L
for n, m being Element of NAT st h . n = x & h . m = y & n <= m holds
y <= x

proof

defpred S₂[ Nat] means for a being Element of NAT
for s, t being Element of L st t = h . a & s = h . $1 & a <= $1 holds
s <= t;
A28: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis:
assume A29: for j being Element of NAT
for s, t being Element of L st t = h . j & s = h . k & j <= k holds
s <= t ; :: thesis:
k in NAT by ORDINAL1:def 12;
then h . k in R by A19, FUNCT_1:def 3;
then reconsider s = h . k as Element of L ;
let a be Element of NAT ; :: thesis:
let c, d be Element of L; :: thesis:
assume that
A30: d = h . a and
A31: c = h . (k + 1) and
A32: a <= k + 1 ; :: thesis:
A33: c <= s by A22, A31;

per cases by A32, NAT_1:8;

suppose a <= k ; :: thesis:

then s <= d by A29, A30;
hence c <= d by A33, ORDERS_2:3; :: thesis:

end;

suppose a = k + 1 ; :: thesis:

hence c <= d by A30, A31; :: thesis:

end;

A34: S₂[ 0 ] by NAT_1:3;
A35: for k being Nat holds S₂[k] from NAT_1:sch 2(A34, A28);
let x, y be Element of L; :: thesis:
let n, m be Element of NAT ; :: thesis:
assume ( h . n = x & h . m = y & n <= m ) ; :: thesis:
hence y <= x by A35; :: thesis:

end;

A36: for x, y being Element of L st x in R & y in R & not x <= y holds
y <= x

proof

let x, y be Element of L; :: thesis:
assume that
A37: x in R and
A38: y in R ; :: thesis:
consider m being object such that
A39: m in dom h and
A40: y = h . m by A38, FUNCT_1:def 3;
reconsider m = m as Element of NAT by A39;
consider n being object such that
A41: n in dom h and
A42: x = h . n by A37, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A41;

per cases ;

suppose m <= n ; :: thesis:

hence ( x <= y or y <= x ) by A27, A42, A40; :: thesis:

end;

suppose n <= m ; :: thesis:

hence ( x <= y or y <= x ) by A27, A42, A40; :: thesis:

end;

A43: uparrow (fininfs R) is Open

proof

let x be Element of L; :: according to WAYBEL_6:def 1 :: thesis:
assume x in uparrow (fininfs R) ; :: thesis:
then consider y being Element of L such that
A44: y <= x and
A45: y in fininfs R by WAYBEL_0:def 16;
consider Y being finite Subset of R such that
A46: y = "/\" (Y,L) and
ex_inf_of Y,L by A45;

per cases ;

suppose Y <> {} ; :: thesis:

then y in Y by A36, A46, Th27;
then consider n being object such that
A47: n in dom h and
A48: h . n = y by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A47;
consider x1, y1 being Element of V1, z1 being Element of L such that
A49: x1 = h . n and
A50: y1 = h . (n + 1) and
z1 = g . (n + 1) and
A51: y1 << x1 "/\" z1 by A18;
take y1 ; :: thesis:
y1 in R by A19, A50, FUNCT_1:def 3;
hence y1 in uparrow (fininfs R) by A21; :: thesis:
x1 "/\" z1 <= x1 by YELLOW_0:23;
then y1 << x1 by A51, WAYBEL_3:2;
hence y1 is_way_below x by A44, A48, A49, WAYBEL_3:2; :: thesis:

end;

suppose A52: Y = {} ; :: thesis:

consider b being object such that
A53: b in R by XBOOLE_0:def 1;
reconsider b = b as Element of L by A53;
consider n being object such that
A54: n in dom h and
h . n = b by A53, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A54;
A55: x <= Top L by YELLOW_0:45;
consider x1, y1 being Element of V1, z1 being Element of L such that
x1 = h . n and
A56: y1 = h . (n + 1) and
z1 = g . (n + 1) and
A57: y1 << x1 "/\" z1 by A18;
y = Top L by A46, A52, YELLOW_0:def 12;
then x = Top L by A44, A55, ORDERS_2:2;
then A58: x1 <= x by YELLOW_0:45;
take y1 ; :: thesis:
y1 in R by A19, A56, FUNCT_1:def 3;
hence y1 in uparrow (fininfs R) by A21; :: thesis:
x1 "/\" z1 <= x1 by YELLOW_0:23;
then y1 << x1 by A57, WAYBEL_3:2;
hence y1 is_way_below x by A58, WAYBEL_3:2; :: thesis:

end;

A59: for n being Element of NAT
for a, b being Element of L st a = g . n & b = g . (n + 1) holds
b <= a

proof

let n be Element of NAT ; :: thesis:
let a, b be Element of L; :: thesis:
assume A60: ( a = g . n & b = g . (n + 1) ) ; :: thesis:
reconsider gn = { (f . m) where m is Element of NAT : m <= n } , gn1 = { (f . k) where k is Element of NAT : k <= n + 1 } as non empty finite Subset of L by Lm1;
A61: ( ex_inf_of gn,L & ex_inf_of gn1,L ) by YELLOW_0:55;
A62: gn c= gn1

proof

let i be object ; :: according to TARSKI:def 3 :: thesis:
assume i in gn ; :: thesis:
then consider k being Element of NAT such that
A63: i = f . k and
A64: k <= n ;
k <= n + 1 by A64, NAT_1:12;
hence i in gn1 by A63; :: thesis:

end;

( a = "/\" (gn,L) & b = "/\" (gn1,L) ) by A5, A60;
hence b <= a by A61, A62, YELLOW_0:35; :: thesis:

end;

A65: AA is_coarser_than R

proof

let a be Element of L; :: according to YELLOW_4:def 2 :: thesis:
assume a in AA ; :: thesis:
then consider x being object such that
A66: x in dom g and
A67: g . x = a by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A66;
consider x1, y1 being Element of V1, z1 being Element of L such that
x1 = h . x and
A68: y1 = h . (x + 1) and
A69: z1 = g . (x + 1) and
A70: y1 << x1 "/\" z1 by A18;
( x1 "/\" z1 <= z1 & y1 <= x1 "/\" z1 ) by A70, WAYBEL_3:1, YELLOW_0:23;
then A71: y1 <= z1 by ORDERS_2:3;
A72: h . (x + 1) in R by A19, FUNCT_1:def 3;
z1 <= a by A59, A67, A69;
hence ex b being Element of L st
( b in R & b <= a ) by A68, A72, A71, ORDERS_2:3; :: thesis:

end;

reconsider O = uparrow (fininfs R) as Open Filter of L by A43;
R is_coarser_than O by A21, Th16;
then A73: AA c= O by A65, YELLOW_4:7, YELLOW_4:8;
take O ; :: thesis:
thus O c= V :: thesis:

proof

let q be object ; :: according to TARSKI:def 3 :: thesis:
assume q in O ; :: thesis:
then reconsider q = q as Element of O ;
consider y being Element of L such that
A74: y <= q and
A75: y in fininfs R by WAYBEL_0:def 16;
consider Y being finite Subset of R such that
A76: y = "/\" (Y,L) and
ex_inf_of Y,L by A75;

per cases ;

suppose Y <> {} ; :: thesis:

then y in Y by A36, A76, Th27;
then consider n being object such that
A77: n in dom h and
A78: h . n = y by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A77;
ex x1, y1 being Element of V1 ex z1 being Element of L st
( x1 = h . n & y1 = h . (n + 1) & z1 = g . (n + 1) & y1 << x1 "/\" z1 ) by A18;
hence q in V by A74, A78, WAYBEL_0:def 20; :: thesis:

end;

suppose A79: Y = {} ; :: thesis:

A80: q <= Top L by YELLOW_0:45;
y = Top L by A76, A79, YELLOW_0:def 12;
then q = Top L by A74, A80, ORDERS_2:2;
hence q in V by Th8; :: thesis:

end;

thus v in O by A17, A20, A21; :: thesis:
uparrow (fininfs AA) = F by A7, Def3;
hence F c= O by A73, WAYBEL_0:62; :: thesis: