let L be lower-bounded continuous LATTICE; 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; 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; 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; ( 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
; 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
; ( x <= p & not p in uparrow ({y} "/\" N) )
thus
x <= p
by A6; 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; verum