let L be lower-bounded continuous LATTICE; :: thesis: for x being Element of L
for N being non empty countable Subset of L st ( for n, y being Element of L st not y <= x & n in N holds
not y "/\" n <= x ) holds
for y being Element of L st not y <= x holds
ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )

let x be Element of L; :: thesis: for N being non empty countable Subset of L st ( for n, y being Element of L st not y <= x & n in N holds
not y "/\" n <= x ) holds
for y being Element of L st not y <= x 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 n, y being Element of L st not y <= x & n in N holds
not y "/\" n <= x ) implies for y being Element of L st not y <= x holds
ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) ) )

assume A1: for n, y being Element of L st not y <= x & n in N holds
not y "/\" n <= x ; :: thesis: for y being Element of L st not y <= x holds
ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )

set V = () ` ;
A2: ((downarrow x) `) "/\" N c= () `
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in (() `) "/\" N or q in () ` )
assume q in (() `) "/\" N ; :: thesis: q in () `
then consider v, n being Element of L such that
A3: q = v "/\" n and
A4: v in () ` and
A5: n in N ;
not v in downarrow x by ;
then not v <= x by WAYBEL_0:17;
then not v "/\" n <= x by A1, A5;
then not v "/\" n in downarrow x by WAYBEL_0:17;
hence q in () ` by ; :: thesis: verum
end;
x <= x ;
then x in downarrow x by WAYBEL_0:17;
then A6: not x in () ` by XBOOLE_0:def 5;
let y be Element of L; :: thesis: ( not y <= x implies ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) ) )

assume not y <= x ; :: thesis: ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )

then not y in downarrow x by WAYBEL_0:17;
then y in () ` by XBOOLE_0:def 5;
hence ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) ) by A2, A6, Th35; :: thesis: verum