let L be complete algebraic LATTICE; :: thesis:
let p be Element of L; :: thesis:
thus ( ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) implies p is completely-irreducible ) by Th26; :: thesis:
thus ( p is completely-irreducible implies ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) ) :: thesis:

proof

defpred S₁[ Element of L] means ( $1 in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & $1 is_maximal_in the carrier of L \ (uparrow k) ) );
reconsider A = { x where x is Element of L : S₁[x] } as Subset of L from DOMAIN_1:sch 7();
assume A1: p is completely-irreducible ; :: thesis:
then p = inf A by Th35;
then p in A by A1, Th34;
then consider x being Element of L such that
A2: x = p and
x in uparrow p and
A3: ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) ;
consider k being Element of L such that
A4: k in the carrier of (CompactSublatt L) and
A5: x is_maximal_in the carrier of L \ (uparrow k) by A3;
take k ; :: thesis:
thus k in the carrier of (CompactSublatt L) by A4; :: thesis:
thus p is_maximal_in the carrier of L \ (uparrow k) by A2, A5; :: thesis:

end;