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 meet-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 meet-irreducible & x <= p & not y <= p ) )
assume A1: not y <= x ; :: thesis: ex p being Element of L st
( p is meet-irreducible & x <= p & not y <= p )
( ( for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ) & L is up-complete & L is satisfying_axiom_of_approximation ) ;
then consider u being Element of L such that
A2: ( u << y & not u <= x ) by A1, WAYBEL_3:24;
consider F being Open Filter of L such that
A3: ( y in F & F c= wayabove u ) by A2, Th8;
A4: wayabove u c= uparrow u by WAYBEL_3:11;

now

assume x in F ; :: thesis: contradiction
then x in uparrow u by A3, A4, TARSKI:def 3;
hence contradiction by A2, WAYBEL_0:18; :: thesis: verum

end;

then x in the carrier of L \ F by XBOOLE_0:def 5;
then consider m being Element of L such that
A5: ( x <= m & m is_maximal_in F ` ) by Th9;
A6: m in F ` by A5, WAYBEL_4:56;

A7: now

assume y <= m ; :: thesis: contradiction
then m in F by A3, WAYBEL_0:def 20;
hence contradiction by A6, XBOOLE_0:def 5; :: thesis: verum

end;

take m ; :: thesis: ( m is meet-irreducible & x <= m & not y <= m )
thus ( m is meet-irreducible & x <= m & not y <= m ) by A5, A7, Th13; :: thesis: verum