let L be lower-bounded continuous LATTICE; :: thesis: for D being non empty countable dense Subset of L

for u being Element of L st u <> Bottom L holds

ex p being irreducible Element of L st

( p <> Top L & not p in uparrow ({u} "/\" D) )

let D be non empty countable dense Subset of L; :: thesis: for u being Element of L st u <> Bottom L holds

ex p being irreducible Element of L st

( p <> Top L & not p in uparrow ({u} "/\" D) )

let u be Element of L; :: thesis: ( u <> Bottom L implies ex p being irreducible Element of L st

( p <> Top L & not p in uparrow ({u} "/\" D) ) )

assume A1: u <> Bottom L ; :: thesis: ex p being irreducible Element of L st

( p <> Top L & not p in uparrow ({u} "/\" D) )

A2: for d, y being Element of L st not y <= Bottom L & d in D holds

not y "/\" d <= Bottom L

then not u <= Bottom L by A1, ORDERS_2:2;

then consider p being irreducible Element of L such that

Bottom L <= p and

A5: not p in uparrow ({u} "/\" D) by A2, Th36;

take p ; :: thesis: ( p <> Top L & not p in uparrow ({u} "/\" D) )

thus p <> Top L by A5, Th9; :: thesis: not p in uparrow ({u} "/\" D)

thus not p in uparrow ({u} "/\" D) by A5; :: thesis: verum

for u being Element of L st u <> Bottom L holds

ex p being irreducible Element of L st

( p <> Top L & not p in uparrow ({u} "/\" D) )

let D be non empty countable dense Subset of L; :: thesis: for u being Element of L st u <> Bottom L holds

ex p being irreducible Element of L st

( p <> Top L & not p in uparrow ({u} "/\" D) )

let u be Element of L; :: thesis: ( u <> Bottom L implies ex p being irreducible Element of L st

( p <> Top L & not p in uparrow ({u} "/\" D) ) )

assume A1: u <> Bottom L ; :: thesis: ex p being irreducible Element of L st

( p <> Top L & not p in uparrow ({u} "/\" D) )

A2: for d, y being Element of L st not y <= Bottom L & d in D holds

not y "/\" d <= Bottom L

proof

Bottom L <= u
by YELLOW_0:44;
let d, y be Element of L; :: thesis: ( not y <= Bottom L & d in D implies not y "/\" d <= Bottom L )

assume A3: not y <= Bottom L ; :: thesis: ( not d in D or not y "/\" d <= Bottom L )

assume d in D ; :: thesis: not y "/\" d <= Bottom L

then d is dense by Def5;

then A4: y "/\" d <> Bottom L by A3;

Bottom L <= y "/\" d by YELLOW_0:44;

hence not y "/\" d <= Bottom L by A4, ORDERS_2:2; :: thesis: verum

end;assume A3: not y <= Bottom L ; :: thesis: ( not d in D or not y "/\" d <= Bottom L )

assume d in D ; :: thesis: not y "/\" d <= Bottom L

then d is dense by Def5;

then A4: y "/\" d <> Bottom L by A3;

Bottom L <= y "/\" d by YELLOW_0:44;

hence not y "/\" d <= Bottom L by A4, ORDERS_2:2; :: thesis: verum

then not u <= Bottom L by A1, ORDERS_2:2;

then consider p being irreducible Element of L such that

Bottom L <= p and

A5: not p in uparrow ({u} "/\" D) by A2, Th36;

take p ; :: thesis: ( p <> Top L & not p in uparrow ({u} "/\" D) )

thus p <> Top L by A5, Th9; :: thesis: not p in uparrow ({u} "/\" D)

thus not p in uparrow ({u} "/\" D) by A5; :: thesis: verum