let L be non empty Poset; :: thesis:
let p be Element of L; :: thesis:
thus ( p is completely-irreducible implies ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) ) ) :: thesis:

proof

assume A1: p is completely-irreducible ; :: thesis:
then ex_min_of (uparrow p) \ {p},L ;
then A2: ex_inf_of (uparrow p) \ {p},L by WAYBEL_1:def 4;
take q = "/\" (((uparrow p) \ {p}),L); :: thesis:

now :: thesis:

let s be Element of L; :: thesis:
assume s in (uparrow p) \ {p} ; :: thesis:
then s in uparrow p by XBOOLE_0:def 5;
hence p <= s by WAYBEL_0:18; :: thesis:

end;

then p is_<=_than (uparrow p) \ {p} by LATTICE3:def 8;
then A3: p <= q by A2, YELLOW_0:def 10;
A4: {p} \/ (uparrow q) c= uparrow p

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A5: x in {p} \/ (uparrow q) ; :: thesis:

now :: thesis:

per cases by A5, XBOOLE_0:def 3;

suppose A6: x in {p} ; :: thesis:

A7: p <= p ;
x = p by A6, TARSKI:def 1;
hence x in uparrow p by A7, WAYBEL_0:18; :: thesis:

end;

suppose A8: x in uparrow q ; :: thesis:

then reconsider x1 = x as Element of L ;
q <= x1 by A8, WAYBEL_0:18;
then p <= x1 by A3, ORDERS_2:3;
hence x in uparrow p by WAYBEL_0:18; :: thesis:

end;

end;

end;

hence x in uparrow p ; :: thesis:

end;

"/\" (((uparrow p) \ {p}),L) <> p by A1, Th19;
hence p < q by A3, ORDERS_2:def 6; :: thesis:
A9: q is_<=_than (uparrow p) \ {p} by A2, YELLOW_0:def 10;
thus for s being Element of L st p < s holds
q <= s :: thesis:

proof

let s be Element of L; :: thesis:
assume A10: p < s ; :: thesis:
then p <= s by ORDERS_2:def 6;
then A11: s in uparrow p by WAYBEL_0:18;
not s in {p} by A10, TARSKI:def 1;
then s in (uparrow p) \ {p} by A11, XBOOLE_0:def 5;
hence q <= s by A9, LATTICE3:def 8; :: thesis:

end;

uparrow p c= {p} \/ (uparrow q)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A12: x in uparrow p ; :: thesis:
then reconsider x1 = x as Element of L ;
( p = x1 or ( x1 in uparrow p & not x1 in {p} ) ) by A12, TARSKI:def 1;
then ( p = x1 or x1 in (uparrow p) \ {p} ) by XBOOLE_0:def 5;
then ( p = x1 or "/\" (((uparrow p) \ {p}),L) <= x1 ) by A9, LATTICE3:def 8;
then ( x in {p} or x in uparrow q ) by TARSKI:def 1, WAYBEL_0:18;
hence x in {p} \/ (uparrow q) by XBOOLE_0:def 3; :: thesis:

end;

hence uparrow p = {p} \/ (uparrow q) by A4; :: thesis:

end;

thus ( ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) ) implies p is completely-irreducible ) :: thesis:

proof

given q being Element of L such that A13: p < q and
A14: for s being Element of L st p < s holds
q <= s and
A15: uparrow p = {p} \/ (uparrow q) ; :: thesis:
A16: not q in {p} by A13, TARSKI:def 1;
ex q being Element of L st
( (uparrow p) \ {p} is_>=_than q & ( for b being Element of L st (uparrow p) \ {p} is_>=_than b holds
q >= b ) )

proof

take q ; :: thesis:

now :: thesis:

let a be Element of L; :: thesis:
assume A17: a in (uparrow p) \ {p} ; :: thesis:
then not a in {p} by XBOOLE_0:def 5;
then A18: a <> p by TARSKI:def 1;
a in uparrow p by A17, XBOOLE_0:def 5;
then p <= a by WAYBEL_0:18;
then p < a by A18, ORDERS_2:def 6;
hence q <= a by A14; :: thesis:

end;

hence (uparrow p) \ {p} is_>=_than q by LATTICE3:def 8; :: thesis:
let b be Element of L; :: thesis:
assume A19: (uparrow p) \ {p} is_>=_than b ; :: thesis:
q <= q ;
then q in uparrow q by WAYBEL_0:18;
then A20: q in {p} \/ (uparrow q) by XBOOLE_0:def 3;
not q in {p} by A13, TARSKI:def 1;
then q in (uparrow p) \ {p} by A15, A20, XBOOLE_0:def 5;
hence q >= b by A19, LATTICE3:def 8; :: thesis:

end;

then A21: ex_inf_of (uparrow p) \ {p},L by YELLOW_0:16;

A22: now :: thesis:

let b be Element of L; :: thesis:
assume A23: b is_<=_than (uparrow p) \ {p} ; :: thesis:
p <= q by A13, ORDERS_2:def 6;
then A24: q in uparrow p by WAYBEL_0:18;
not q in {p} by A13, TARSKI:def 1;
then q in (uparrow p) \ {p} by A24, XBOOLE_0:def 5;
hence q >= b by A23, LATTICE3:def 8; :: thesis:

end;

p <= q by A13, ORDERS_2:def 6;
then A25: q in uparrow p by WAYBEL_0:18;

now :: thesis:

let c be Element of L; :: thesis:
assume c in (uparrow p) \ {p} ; :: thesis:
then ( c in uparrow p & not c in {p} ) by XBOOLE_0:def 5;
then c in uparrow q by A15, XBOOLE_0:def 3;
hence q <= c by WAYBEL_0:18; :: thesis:

end;

then q is_<=_than (uparrow p) \ {p} by LATTICE3:def 8;
then q = "/\" (((uparrow p) \ {p}),L) by A22, YELLOW_0:31;
then "/\" (((uparrow p) \ {p}),L) in (uparrow p) \ {p} by A25, A16, XBOOLE_0:def 5;
then ex_min_of (uparrow p) \ {p},L by A21, WAYBEL_1:def 4;
hence p is completely-irreducible ; :: thesis:

end;