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 Th23, Th24, Th25;

A3: N c= G

then consider F being Filter of L such that

A8: N is GeneratorSet of F ;

F = uparrow (fininfs N) by A8, Def3;

then A9: F c= G by A3, WAYBEL_0:62;

V "/\" F c= V

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 )

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 Th23, Th24, Th25;

A3: N c= G

proof

N is GeneratorSet of uparrow (fininfs N)
by Def3;
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

end;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

hence
q in G
; :: thesis: verum
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;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

then consider F being Filter of L such that

A8: N is GeneratorSet of F ;

F = uparrow (fininfs N) by A8, Def3;

then A9: F c= G by A3, WAYBEL_0:62;

V "/\" F c= V

proof

then consider O being Open Filter of L such that
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 A9, A12;

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 A11, A13;

hence q in V by A10, A14; :: thesis: verum

end;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 A9, A12;

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 A11, A13;

hence q in V by A10, A14; :: thesis: verum

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

thus
( O c= V & v in O )
by A15, A16; :: thesis: verum
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 A8, Lm4;

then N c= O by A17;

then v "/\" n in O "/\" O by A16, A20;

hence q in O by A19, Th21; :: thesis: verum

end;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 A8, Lm4;

then N c= O by A17;

then v "/\" n in O "/\" O by A16, A20;

hence q in O by A19, Th21; :: thesis: verum