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 ; :: thesis: verum
end;
Bottom L <= u by YELLOW_0:44;
then not u <= Bottom L by ;
then consider p being irreducible Element of L such that
Bottom L <= p and
A5: not p in uparrow ({u} "/\" D) by ;
take p ; :: thesis: ( p <> Top L & not p in uparrow ({u} "/\" D) )
thus p <> Top L by ; :: thesis: not p in uparrow ({u} "/\" D)
thus not p in uparrow ({u} "/\" D) by A5; :: thesis: verum