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 = (downarrow x) ` ;
A2: ((downarrow x) `) "/\" N c= (downarrow x) `

proof

let q be object ; :: 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
A3: q = v "/\" n and
A4: v in (downarrow x) ` and
A5: n in N ;
not v in downarrow x by A4, XBOOLE_0:def 5;
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 (downarrow x) ` by A3, XBOOLE_0:def 5; :: thesis: verum

end;

x <= x ;
then x in downarrow x by WAYBEL_0:17;
then A6: not x in (downarrow x) ` 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 (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 A2, A6, Th35; :: thesis: verum