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
k <= p "\/" k by YELLOW_0:22;
then A2: p "\/" k in uparrow k by WAYBEL_0:18;
p <= p "\/" k by YELLOW_0:22;
then p "\/" k in uparrow p by WAYBEL_0:18;
then A3: ( ex_inf_of (uparrow p) \ {p},L & p "\/" k in (uparrow p) /\ (uparrow k) ) by A2, XBOOLE_0:def 4, YELLOW_0:17;
A4: (uparrow p) \ {p} = (uparrow p) /\ (uparrow k) by A1, Th3;
then "/\" (((uparrow p) \ {p}),L) = p "\/" k by Th1;
then ex_min_of (uparrow p) \ {p},L by A4, A3, WAYBEL_1:def 4;
hence p is completely-irreducible ; :: thesis: verum