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

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

let N be non empty countable Subset of L; :: thesis: for v being Element of L st V "/\" N c= V & v in V holds
ex O being Open Filter of L st
( {v} "/\" N c= O & O c= V & v in O )

let v be Element of L; :: thesis: ( V "/\" N c= V & v in V implies ex O being Open Filter of L st
( {v} "/\" N c= O & O c= V & v in O ) )

assume that
A1: V "/\" N c= V and
A2: v in V ; :: thesis: ex O being Open Filter of L st
( {v} "/\" N c= O & O c= V & v in O )

reconsider G = { x where x is Element of L : V "/\" {x} c= V } as Filter of L by ;
A3: N c= G
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in N or q in G )
assume A4: q in N ; :: thesis: q in G
then reconsider q1 = q as Element of L ;
A5: {q1} "/\" V = { (q1 "/\" y) where y is Element of L : y in V } by YELLOW_4:42;
V "/\" {q1} c= V
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in V "/\" {q1} or t in V )
assume t in V "/\" {q1} ; :: thesis: t in V
then consider y being Element of L such that
A6: t = q1 "/\" y and
A7: y in V by A5;
q1 "/\" y in N "/\" V by A4, A7;
hence t in V by A1, A6; :: thesis: verum
end;
hence q in G ; :: thesis: verum
end;
N is GeneratorSet of uparrow () by Def3;
then consider F being Filter of L such that
A8: N is GeneratorSet of F ;
F = uparrow () by ;
then A9: F c= G by ;
V "/\" F c= V
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in V "/\" F or q in V )
assume q in V "/\" F ; :: thesis: q in V
then consider d, f being Element of L such that
A10: q = d "/\" f and
A11: d in V and
A12: f in F ;
f in G by ;
then consider x being Element of L such that
A13: f = x and
A14: V "/\" {x} c= V ;
x in {x} by TARSKI:def 1;
then d "/\" f in V "/\" {x} by ;
hence q in V by ; :: thesis: verum
end;
then consider O being Open Filter of L such that
A15: O c= V and
A16: v in O and
A17: F c= O by A2, A8, Th33;
take O ; :: thesis: ( {v} "/\" N c= O & O c= V & v in O )
A18: {v} "/\" N = { (v "/\" n) where n is Element of L : n in N } by YELLOW_4:42;
thus {v} "/\" N c= O :: thesis: ( O c= V & v in O )
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {v} "/\" N or q in O )
assume q in {v} "/\" N ; :: thesis: q in O
then consider n being Element of L such that
A19: q = v "/\" n and
A20: n in N by A18;
N c= F by ;
then N c= O by A17;
then v "/\" n in O "/\" O by ;
hence q in O by ; :: thesis: verum
end;
thus ( O c= V & v in O ) by ; :: thesis: verum