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;
given A being non empty GeneratorSet of F such that A3: A is countable ; :: thesis:
reconsider G = { x where x is Element of L : V "/\" {x} c= V } as Filter of L by Th27, Th28, Th29;
A4: F c= G

proof

let q be set ; :: according to TARSKI:def 3 :: thesis:
assume A5: q in F ; :: thesis:
then reconsider s = q as Element of L ;
A6: 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 set ; :: according to TARSKI:def 3 :: thesis:
assume w in V "/\" {s} ; :: thesis:
then consider t being Element of L such that
A7: w = s "/\" t and
A8: t in V by A6;
t "/\" s in V "/\" F by A5, A8;
hence w in V by A1, A7; :: thesis:

end;

hence q in G ; :: thesis:

end;

consider f being Function of NAT ,A such that
A9: rng f = A by A3, CARD_3:146;
reconsider f = f as Function of NAT ,the carrier of L by FUNCT_2:9;
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 Function of NAT ,the carrier of L such that
A10: for n being Element of NAT holds g . n = H₁(n) from FUNCT_2:sch 4();
A11: dom g = NAT by FUNCT_2:def 1;
then reconsider AA = rng g as non empty Subset of L by RELAT_1:65;
A12: 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 A13: ( 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;
A14: ( a = "/\" gn,L & b = "/\" gn1,L ) by A10, A13;
A15: ( ex_inf_of gn,L & ex_inf_of gn1,L ) by YELLOW_0:55;
gn c= gn1

proof

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

end;

hence b <= a by A14, A15, YELLOW_0:35; :: thesis:

end;

A18: AA is GeneratorSet of F by A9, A10, Th36;
then A19: uparrow (fininfs AA) = F by Def3;
defpred S₁[ Element of 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 );
A20: for n being Element of NAT
for x being Element of V1 ex y being Element of V1 st S₁[n,x,y]

proof

let n be Element of NAT ; :: thesis:
let x be Element of V1; :: thesis:
A21: g . (n + 1) in AA by A11, FUNCT_1:def 5;
AA c= F by A18, Lm4;
then AA c= G by A4, XBOOLE_1:1;
then g . (n + 1) in G by A21;
then consider g1 being Element of L such that
A22: g . (n + 1) = g1 and
A23: 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 A23, WAYBEL_6:def 1;
hence ex y being Element of V1 st S₁[n,x,y] by A22; :: thesis:

end;

consider h being Function of NAT ,V1 such that
A24: h . 0 = v1 and
A25: for n being Element of NAT holds S₁[n,h . n,h . (n + 1)] from RECDEF_1:sch 2(A20);
A26: dom h = NAT by FUNCT_2:def 1;
then A27: h . 0 in rng h by FUNCT_1:def 5;
then reconsider R = rng h as non empty Subset of L by XBOOLE_1:1;
set O = uparrow (fininfs R);
A28: for x, y being Element of L
for n being Element of NAT st h . n = x & h . (n + 1) = y holds
y <= x

proof

let x, y be Element of L; :: thesis:
let n be Element of NAT ; :: thesis:
assume A29: ( h . n = x & h . (n + 1) = y ) ; :: thesis:
consider x1, y1 being Element of V1, z1 being Element of L such that
A30: ( x1 = h . n & y1 = h . (n + 1) & z1 = g . (n + 1) & y1 << x1 "/\" z1 ) by A25;
A31: y1 <= x1 "/\" z1 by A30, WAYBEL_3:1;
x1 "/\" z1 <= x1 by YELLOW_0:23;
hence y <= x by A29, A30, A31, ORDERS_2:26; :: thesis:

end;

A32: 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

let x, y be Element of L; :: thesis:
let n, m be Element of NAT ; :: thesis:
assume A33: ( h . n = x & h . m = y & n <= m ) ; :: thesis:
defpred S₂[ Element of 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;
A34: S₂[ 0 ] by NAT_1:3;
A35: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A36: 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:
let a be Element of NAT ; :: thesis:
let c, d be Element of L; :: thesis:
assume A37: ( d = h . a & c = h . (k + 1) & a <= k + 1 ) ; :: thesis:
h . k in R by A26, FUNCT_1:def 5;
then reconsider s = h . k as Element of L ;
A38: c <= s by A28, A37;

per cases by A37, NAT_1:8;

suppose a <= k ; :: thesis:

then s <= d by A36, A37;
hence c <= d by A38, ORDERS_2:26; :: thesis:

end;

suppose a = k + 1 ; :: thesis:

hence c <= d by A37; :: thesis:

end;

for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A34, A35);
hence y <= x by A33; :: thesis:

end;

A39: 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 A40: ( x in R & y in R ) ; :: thesis:
then consider n being set such that
A41: n in dom h and
A42: x = h . n by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A41;
consider m being set such that
A43: m in dom h and
A44: y = h . m by A40, FUNCT_1:def 5;
reconsider m = m as Element of NAT by A43;

per cases ;

suppose m <= n ; :: thesis:

hence ( x <= y or y <= x ) by A32, A42, A44; :: thesis:

end;

suppose n <= m ; :: thesis:

hence ( x <= y or y <= x ) by A32, A42, A44; :: thesis:

end;

A45: R c= uparrow (fininfs R) by WAYBEL_0:62;
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
A46: y <= x and
A47: y in fininfs R by WAYBEL_0:def 16;
consider Y being finite Subset of R such that
A48: y = "/\" Y,L and
ex_inf_of Y,L by A47;

per cases ;

suppose Y <> {} ; :: thesis:

then y in Y by A39, A48, Th31;
then consider n being set such that
A49: n in dom h and
A50: h . n = y by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A49;
consider x1, y1 being Element of V1, z1 being Element of L such that
A51: x1 = h . n and
A52: y1 = h . (n + 1) and
z1 = g . (n + 1) and
A53: y1 << x1 "/\" z1 by A25;
take y1 ; :: thesis:
y1 in R by A26, A52, FUNCT_1:def 5;
hence y1 in uparrow (fininfs R) by A45; :: thesis:
x1 "/\" z1 <= x1 by YELLOW_0:23;
then y1 << x1 by A53, WAYBEL_3:2;
hence y1 is_way_below x by A46, A50, A51, WAYBEL_3:2; :: thesis:

end;

suppose Y = {} ; :: thesis:

then A54: y = Top L by A48, YELLOW_0:def 12;
x <= Top L by YELLOW_0:45;
then A55: x = Top L by A46, A54, ORDERS_2:25;
consider b being set such that
A56: b in R by XBOOLE_0:def 1;
reconsider b = b as Element of L by A56;
consider n being set such that
A57: n in dom h and
h . n = b by A56, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A57;
consider x1, y1 being Element of V1, z1 being Element of L such that
x1 = h . n and
A58: y1 = h . (n + 1) and
z1 = g . (n + 1) and
A59: y1 << x1 "/\" z1 by A25;
take y1 ; :: thesis:
y1 in R by A26, A58, FUNCT_1:def 5;
hence y1 in uparrow (fininfs R) by A45; :: thesis:
x1 "/\" z1 <= x1 by YELLOW_0:23;
then A60: y1 << x1 by A59, WAYBEL_3:2;
x1 <= x by A55, YELLOW_0:45;
hence y1 is_way_below x by A60, WAYBEL_3:2; :: thesis:

end;

then reconsider O = uparrow (fininfs R) as Open Filter of L ;
take O ; :: thesis:
thus O c= V :: thesis:

proof

let q be set ; :: 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
A61: y <= q and
A62: y in fininfs R by WAYBEL_0:def 16;
consider Y being finite Subset of R such that
A63: y = "/\" Y,L and
ex_inf_of Y,L by A62;

per cases ;

suppose Y <> {} ; :: thesis:

then y in Y by A39, A63, Th31;
then consider n being set such that
A64: n in dom h and
A65: h . n = y by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A64;
consider x1, y1 being Element of V1, z1 being Element of L such that
A66: x1 = h . n and
( y1 = h . (n + 1) & z1 = g . (n + 1) & y1 << x1 "/\" z1 ) by A25;
thus q in V by A61, A65, A66, WAYBEL_0:def 20; :: thesis:

end;

suppose Y = {} ; :: thesis:

then A67: y = Top L by A63, YELLOW_0:def 12;
q <= Top L by YELLOW_0:45;
then q = Top L by A61, A67, ORDERS_2:25;
hence q in V by Th12; :: thesis:

end;

thus v in O by A24, A27, A45; :: thesis:
A68: 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 set such that
A69: x in dom g and
A70: g . x = a by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A69;
consider x1, y1 being Element of V1, z1 being Element of L such that
x1 = h . x and
A71: y1 = h . (x + 1) and
A72: z1 = g . (x + 1) and
A73: y1 << x1 "/\" z1 by A25;
A74: h . (x + 1) in R by A26, FUNCT_1:def 5;
A75: x1 "/\" z1 <= z1 by YELLOW_0:23;
y1 <= x1 "/\" z1 by A73, WAYBEL_3:1;
then A76: y1 <= z1 by A75, ORDERS_2:26;
z1 <= a by A12, A70, A72;
hence ex b being Element of L st
( b in R & b <= a ) by A71, A74, A76, ORDERS_2:26; :: thesis:

end;

R is_coarser_than O by A45, Th20;
then AA c= O by A68, YELLOW_4:7, YELLOW_4:8;
hence F c= O by A19, WAYBEL_0:62; :: thesis: