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) `

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

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

x <= x
;
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;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

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