let L be lower-bounded algebraic LATTICE; :: thesis: for x, y being Element of L st not y <= x holds
ex p being Element of L st
( p is completely-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 completely-irreducible & x <= p & not y <= p ) )
assume A1: not y <= x ; :: thesis: ex p being Element of L st
( p is completely-irreducible & x <= p & not y <= p )
for z being Element of L holds
( not waybelow z is empty & waybelow z is directed ) ;
then consider k1 being Element of L such that
A2: k1 << y and
A3: not k1 <= x by A1, WAYBEL_3:24;
consider k being Element of L such that
A4: k in the carrier of (CompactSublatt L) and
A5: k1 <= k and
A6: k <= y by A2, WAYBEL_8:7;
not k <= x by A3, A5, ORDERS_2:3;
then not x in uparrow k by WAYBEL_0:18;
then x in the carrier of L \ (uparrow k) by XBOOLE_0:def 5;
then A7: x in (uparrow k) ` by SUBSET_1:def 4;
k is compact by A4, WAYBEL_8:def 1;
then uparrow k is Open Filter of L by WAYBEL_8:2;
then consider p being Element of L such that
A8: x <= p and
A9: p is_maximal_in (uparrow k) ` by A7, WAYBEL_6:9;
take p ; :: thesis: ( p is completely-irreducible & x <= p & not y <= p )
the carrier of L \ (uparrow k) = (uparrow k) ` by SUBSET_1:def 4;
hence p is completely-irreducible by A9, Th26; :: thesis: ( x <= p & not y <= p )
thus x <= p by A8; :: thesis: not y <= p
thus not y <= p :: thesis: verum

proof

p in (uparrow k) ` by A9, WAYBEL_4:55;
then p in the carrier of L \ (uparrow k) by SUBSET_1:def 4;
then A10: not p in uparrow k by XBOOLE_0:def 5;
assume y <= p ; :: thesis: contradiction
then k <= p by A6, ORDERS_2:3;
hence contradiction by A10, WAYBEL_0:18; :: thesis: verum

end;