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

proof

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;

Bottom L <= u by YELLOW_0:44;
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