let L be lower-bounded continuous LATTICE; :: thesis: for V being upper Open Subset of L
for F being Filter of L
for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds
ex O being Open Filter of L st
( O c= V & v in O & F c= O )

let V be upper Open Subset of L; :: thesis: for F being Filter of L
for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds
ex O being Open Filter of L st
( O c= V & v in O & F c= O )

let F be Filter of L; :: thesis: for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds
ex O being Open Filter of L st
( O c= V & v in O & F c= O )

let v be Element of L; :: thesis: ( V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable implies ex O being Open Filter of L st
( O c= V & v in O & F c= O ) )

assume that
A1: V "/\" F c= V and
A2: v in V ; :: thesis: ( for A being non empty GeneratorSet of F holds not A is countable or ex O being Open Filter of L st
( O c= V & v in O & F c= O ) )

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 ;
given A being non empty GeneratorSet of F such that A3: A is countable ; :: thesis: ex O being Open Filter of L st
( O c= V & v in O & F c= O )

consider f being sequence of A such that
A4: rng f = A by ;
reconsider f = f as sequence of the carrier of L by FUNCT_2:7;
deffunc H1( 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 = H1(n) from defpred S1[ 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: ( not q in F or q in G )
assume A9: q in F ; :: thesis: q in G
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: ( not w in V "/\" {s} or w in V )
assume w in V "/\" {s} ; :: thesis: w in V
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 ;
hence w in V by ; :: thesis: verum
end;
hence q in G ; :: thesis: verum
end;
A13: for n being Nat
for x being Element of V1 ex y being Element of V1 st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of V1 ex y being Element of V1 st S1[n,x,y]
let x be Element of V1; :: thesis: ex y being Element of V1 st S1[n,x,y]
AA c= F by ;
then A14: AA c= G by A8;
g . (n + 1) in AA by ;
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 ;
hence ex y being Element of V1 st S1[n,x,y] by A15; :: thesis: verum
end;
consider h being sequence of V1 such that
A17: h . 0 = v1 and
A18: for n being Nat holds S1[n,h . n,h . (n + 1)] from 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 ();
A21: R c= uparrow () 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: for n being Nat st h . n = x & h . (n + 1) = y holds
y <= x

let n be Nat; :: thesis: ( h . n = x & h . (n + 1) = y implies y <= x )
assume A23: ( h . n = x & h . (n + 1) = y ) ; :: thesis: y <= x
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 ;
hence y <= x by ; :: thesis: verum
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 S2[ 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 S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
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: S2[k + 1]
k in NAT by ORDINAL1:def 12;
then h . k in R by ;
then reconsider s = h . k as Element of L ;
let a be Element of NAT ; :: thesis: for s, t being Element of L st t = h . a & s = h . (k + 1) & a <= k + 1 holds
s <= t

let c, d be Element of L; :: thesis: ( d = h . a & c = h . (k + 1) & a <= k + 1 implies c <= d )
assume that
A30: d = h . a and
A31: c = h . (k + 1) and
A32: a <= k + 1 ; :: thesis: c <= d
A33: c <= s by ;
per cases ( a <= k or a = k + 1 ) by ;
suppose a <= k ; :: thesis: c <= d
then s <= d by ;
hence c <= d by ; :: thesis: verum
end;
suppose a = k + 1 ; :: thesis: c <= d
hence c <= d by ; :: thesis: verum
end;
end;
end;
A34: S2[ 0 ] by NAT_1:3;
A35: for k being Nat holds S2[k] from let x, y be Element of L; :: thesis: for n, m being Element of NAT st h . n = x & h . m = y & n <= m holds
y <= x

let n, m be Element of NAT ; :: thesis: ( h . n = x & h . m = y & n <= m implies y <= x )
assume ( h . n = x & h . m = y & n <= m ) ; :: thesis: y <= x
hence y <= x by A35; :: thesis: verum
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: ( x in R & y in R & not x <= y implies y <= x )
assume that
A37: x in R and
A38: y in R ; :: thesis: ( x <= y or y <= x )
consider m being object such that
A39: m in dom h and
A40: y = h . m by ;
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 ;
reconsider n = n as Element of NAT by A41;
per cases ( m <= n or n <= m ) ;
suppose m <= n ; :: thesis: ( x <= y or y <= x )
hence ( x <= y or y <= x ) by ; :: thesis: verum
end;
suppose n <= m ; :: thesis: ( x <= y or y <= x )
hence ( x <= y or y <= x ) by ; :: thesis: verum
end;
end;
end;
A43: uparrow () is Open
proof
let x be Element of L; :: according to WAYBEL_6:def 1 :: thesis: ( not x in uparrow () or ex b1 being Element of the carrier of L st
( b1 in uparrow () & b1 is_way_below x ) )

assume x in uparrow () ; :: thesis: ex b1 being Element of the carrier of L st
( b1 in uparrow () & b1 is_way_below x )

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 ( Y <> {} or Y = {} ) ;
suppose Y <> {} ; :: thesis: ex b1 being Element of the carrier of L st
( b1 in uparrow () & b1 is_way_below x )

then y in Y by ;
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 uparrow () & y1 is_way_below x )
y1 in R by ;
hence y1 in uparrow () by A21; :: thesis: y1 is_way_below x
x1 "/\" z1 <= x1 by YELLOW_0:23;
then y1 << x1 by ;
hence y1 is_way_below x by ; :: thesis: verum
end;
suppose A52: Y = {} ; :: thesis: ex b1 being Element of the carrier of L st
( b1 in uparrow () & b1 is_way_below x )

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 ;
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 ;
then x = Top L by ;
then A58: x1 <= x by YELLOW_0:45;
take y1 ; :: thesis: ( y1 in uparrow () & y1 is_way_below x )
y1 in R by ;
hence y1 in uparrow () by A21; :: thesis: y1 is_way_below x
x1 "/\" z1 <= x1 by YELLOW_0:23;
then y1 << x1 by ;
hence y1 is_way_below x by ; :: thesis: verum
end;
end;
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: for a, b being Element of L st a = g . n & b = g . (n + 1) holds
b <= a

let a, b be Element of L; :: thesis: ( a = g . n & b = g . (n + 1) implies b <= a )
assume A60: ( a = g . n & b = g . (n + 1) ) ; :: thesis: b <= a
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: ( not i in gn or i in gn1 )
assume i in gn ; :: thesis: i in gn1
then consider k being Element of NAT such that
A63: i = f . k and
A64: k <= n ;
k <= n + 1 by ;
hence i in gn1 by A63; :: thesis: verum
end;
( a = "/\" (gn,L) & b = "/\" (gn1,L) ) by ;
hence b <= a by ; :: thesis: verum
end;
A65: AA is_coarser_than R
proof
let a be Element of L; :: according to YELLOW_4:def 2 :: thesis: ( not a in AA or ex b1 being Element of the carrier of L st
( b1 in R & b1 <= a ) )

assume a in AA ; :: thesis: ex b1 being Element of the carrier of L st
( b1 in R & b1 <= a )

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 ;
then A71: y1 <= z1 by ORDERS_2:3;
A72: h . (x + 1) in R by ;
z1 <= a by ;
hence ex b being Element of L st
( b in R & b <= a ) by ; :: thesis: verum
end;
reconsider O = uparrow () as Open Filter of L by A43;
R is_coarser_than O by ;
then A73: AA c= O by ;
take O ; :: thesis: ( O c= V & v in O & F c= O )
thus O c= V :: thesis: ( v in O & F c= O )
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in O or q in V )
assume q in O ; :: thesis: q in V
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 ( Y <> {} or Y = {} ) ;
suppose Y <> {} ; :: thesis: q in V
then y in Y by ;
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 ; :: thesis: verum
end;
end;
end;
thus v in O by ; :: thesis: F c= O
uparrow (fininfs AA) = F by ;
hence F c= O by ; :: thesis: verum