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