let L be complete algebraic LATTICE; :: thesis: for p being Element of L holds
( ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) iff p is completely-irreducible )
let p be Element of L; :: thesis: ( ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) iff p is completely-irreducible )
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: ( 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) ) )
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: verum

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: ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )
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: ( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )
thus k in the carrier of (CompactSublatt L) by A4; :: thesis: p is_maximal_in the carrier of L \ (uparrow k)
thus p is_maximal_in the carrier of L \ (uparrow k) by A2, A5; :: thesis: verum

end;