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