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) )
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 A2: not y <= x ; :: thesis: ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )
set V = (downarrow x) ` ;
A3: ((downarrow x) ` ) "/\" N c= (downarrow x) `

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in ((downarrow x) ` ) "/\" N or q in (downarrow x) ` )
assume q in ((downarrow x) ` ) "/\" N ; :: thesis: q in (downarrow x) `
then consider v, n being Element of L such that
A4: q = v "/\" n and
A5: v in (downarrow x) ` and
A6: n in N ;
not v in downarrow x by A5, XBOOLE_0:def 5;
then not v <= x by WAYBEL_0:17;
then not v "/\" n <= x by A1, A6;
then not v "/\" n in downarrow x by WAYBEL_0:17;
hence q in (downarrow x) ` by A4, XBOOLE_0:def 5; :: thesis: verum

end;

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