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, Th34;

( uparrow O c= O & O c= uparrow O ) by WAYBEL_0:16, WAYBEL_0:24;

then uparrow O = O ;

then A5: uparrow ({y} "/\" N) c= O by A3, YELLOW_3:7;

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

A6: x <= p and

A7: p is_maximal_in O ` by WAYBEL_6:9;

reconsider p = p as irreducible Element of L by A7, WAYBEL_6:13;

take p ; :: thesis: ( x <= p & not p in uparrow ({y} "/\" N) )

thus x <= p by A6; :: thesis: not p in uparrow ({y} "/\" N)

p in O ` by A7, WAYBEL_4:55;

hence not p in uparrow ({y} "/\" N) by A5, XBOOLE_0:def 5; :: thesis: verum

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, Th34;

( uparrow O c= O & O c= uparrow O ) by WAYBEL_0:16, WAYBEL_0:24;

then uparrow O = O ;

then A5: uparrow ({y} "/\" N) c= O by A3, YELLOW_3:7;

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

A6: x <= p and

A7: p is_maximal_in O ` by WAYBEL_6:9;

reconsider p = p as irreducible Element of L by A7, WAYBEL_6:13;

take p ; :: thesis: ( x <= p & not p in uparrow ({y} "/\" N) )

thus x <= p by A6; :: thesis: not p in uparrow ({y} "/\" N)

p in O ` by A7, WAYBEL_4:55;

hence not p in uparrow ({y} "/\" N) by A5, XBOOLE_0:def 5; :: thesis: verum