let L be lower-bounded continuous LATTICE; :: thesis: for x, y being Element of L st not y <= x holds
ex p being Element of L st
( p is irreducible & x <= p & not y <= p )
let x, y be Element of L; :: thesis: ( not y <= x implies ex p being Element of L st
( p is irreducible & x <= p & not y <= p ) )
assume A1: not y <= x ; :: thesis: ex p being Element of L st
( p is irreducible & x <= p & not y <= p )
for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ;
then consider u being Element of L such that
A2: u << y and
A3: not u <= x by A1, WAYBEL_3:24;
consider F being Open Filter of L such that
A4: y in F and
A5: F c= wayabove u by A2, Th8;
A6: wayabove u c= uparrow u by WAYBEL_3:11;
not x in F by A3, WAYBEL_0:18, A5, A6;
then x in the carrier of L \ F by XBOOLE_0:def 5;
then consider m being Element of L such that
A7: x <= m and
A8: m is_maximal_in F ` by Th9;
take m ; :: thesis: ( m is irreducible & x <= m & not y <= m )
A9: m in F ` by A8, WAYBEL_4:55;
now :: thesis: not y <= m
assume y <= m ; :: thesis: contradiction
then m in F by A4, WAYBEL_0:def 20;
hence contradiction by A9, XBOOLE_0:def 5; :: thesis: verum
end;
hence ( m is irreducible & x <= m & not y <= m ) by A7, A8, Th13; :: thesis: verum