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 x, y being Element of L st V "/\" N c= V & y in V & not x in V holds
ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )
let V be upper Open Subset of L; :: thesis: for N being non empty countable Subset of L
for x, y being Element of L st V "/\" N c= V & y in V & not x in V holds
ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )
let N be non empty countable Subset of L; :: thesis: for x, y being Element of L st V "/\" N c= V & y in V & not x in V holds
ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )
let x, y be Element of L; :: thesis: ( V "/\" N c= V & y in V & not x in V implies ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) ) )
assume that
A1: ( V "/\" N c= V & y in V ) and
A2: not x in V ; :: thesis: ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )
consider O being Open Filter of L such that
A3: {y} "/\" N c= O and
A4: O c= V and
y in O by A1, Th38;
not x in O by A2, A4;
then x in O ` by XBOOLE_0:def 5;
then consider p being Element of L such that
A5: x <= p and
A6: p is_maximal_in O ` by WAYBEL_6:9;
reconsider p = p as irreducible Element of L by A6, WAYBEL_6:13;
take p ; :: thesis: ( x <= p & not p in uparrow ({y} "/\" N) )
thus x <= p by A5; :: thesis: not p in uparrow ({y} "/\" N)
uparrow O = O

proof

thus uparrow O c= O by WAYBEL_0:24; :: according to XBOOLE_0:def 10 :: thesis: O c= uparrow O
thus O c= uparrow O by WAYBEL_0:16; :: thesis: verum

end;

then A7: uparrow ({y} "/\" N) c= O by A3, YELLOW_3:7;
p in O ` by A6, WAYBEL_4:56;
hence not p in uparrow ({y} "/\" N) by A7, XBOOLE_0:def 5; :: thesis: verum