let L be non empty Poset; for p being Element of L holds
( p is completely-irreducible iff 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) ) )
let p be Element of L; ( p is completely-irreducible iff 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) ) )
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) ) )
( 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 )
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 )
verumproof
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)
;
p is completely-irreducible
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 ) )
then A21:
ex_inf_of (uparrow p) \ {p},
L
by YELLOW_0:16;
p <= q
by A13, ORDERS_2:def 6;
then A25:
q in uparrow p
by WAYBEL_0:18;
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
;
verum
end;