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:

assume A1: p is completely-irreducible ; :: thesis:
then A2: ex_min_of (uparrow p) \ {p},L by Def3;
A3: "/\" ((uparrow p) \ {p}),L <> p by A1, Th19;
take q = "/\" ((uparrow p) \ {p}),L; :: thesis:
A4: ex_inf_of (uparrow p) \ {p},L by A2, WAYBEL_1:def 4;
then A5: q is_<=_than (uparrow p) \ {p} by YELLOW_0:def 10;

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 A6: p <= q by A4, YELLOW_0:def 10;
hence p < q by A3, ORDERS_2:def 10; :: thesis:
thus for s being Element of L st p < s holds
q <= s :: thesis:

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

end;

thus uparrow p = {p} \/ (uparrow q) :: thesis:

thus uparrow p c= {p} \/ (uparrow q) :: according to XBOOLE_0:def 10 :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A9: 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 A9, 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 A5, 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;

thus {p} \/ (uparrow q) c= uparrow p :: thesis:

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

per cases by A10, XBOOLE_0:def 3;

suppose x in {p} ; :: thesis:

then ( x = p & p <= p ) by TARSKI:def 1;
hence x in uparrow p by WAYBEL_0:18; :: thesis:

end;

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

then reconsider x1 = x as Element of L ;
q <= x1 by A11, WAYBEL_0:18;
then p <= x1 by A6, ORDERS_2:26;
hence x in uparrow p by WAYBEL_0:18; :: thesis:

end;

hence x in uparrow p ; :: 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:

given q being Element of L such that A12: p < q and
A13: for s being Element of L st p < s holds
q <= s and
A14: uparrow p = {p} \/ (uparrow q) ; :: thesis:
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 ) )

take q ; :: thesis:

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

end;

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

end;

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

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 A14, XBOOLE_0:def 3;
hence q <= c by WAYBEL_0:18; :: thesis:

end;

then A17: q is_<=_than (uparrow p) \ {p} by LATTICE3:def 8;

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

end;

then A19: q = "/\" ((uparrow p) \ {p}),L by A17, YELLOW_0:31;
( p <= q & p <> q ) by A12, ORDERS_2:def 10;
then ( q in uparrow p & not q in {p} ) by TARSKI:def 1, WAYBEL_0:18;
then "/\" ((uparrow p) \ {p}),L in (uparrow p) \ {p} by A19, XBOOLE_0:def 5;
then ex_min_of (uparrow p) \ {p},L by A16, WAYBEL_1:def 4;
hence p is completely-irreducible by Def3; :: thesis:

end;