let L be complete LATTICE; :: thesis: for p being Element of L st ex k being Element of L st p is_maximal_in the carrier of L \ (uparrow k) holds
p is completely-irreducible
let p be Element of L; :: thesis: ( ex k being Element of L st p is_maximal_in the carrier of L \ (uparrow k) implies p is completely-irreducible )
given k being Element of L such that A1: p is_maximal_in the carrier of L \ (uparrow k) ; :: thesis: p is completely-irreducible
A2: (uparrow p) \ {p} = (uparrow p) /\ (uparrow k) by A1, Th3;
then A3: "/\" ((uparrow p) \ {p}),L = p "\/" k by Th1;
A4: ex_inf_of (uparrow p) \ {p},L by YELLOW_0:17;
( p <= p "\/" k & k <= p "\/" k ) by YELLOW_0:22;
then ( p "\/" k in uparrow p & p "\/" k in uparrow k ) by WAYBEL_0:18;
then p "\/" k in (uparrow p) /\ (uparrow k) by XBOOLE_0:def 4;
then ex_min_of (uparrow p) \ {p},L by A2, A3, A4, WAYBEL_1:def 4;
hence p is completely-irreducible by Def3; :: thesis: verum