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;

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

hence
( m is irreducible & x <= m & not y <= m )
by A7, A8, Th13; :: thesis: verumassume
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;then m in F by A4, WAYBEL_0:def 20;

hence contradiction by A9, XBOOLE_0:def 5; :: thesis: verum