let L be non empty Poset; :: thesis: for x being Element of L st x is completely-irreducible holds
for X being Subset of L st ex_inf_of X,L & x = inf X holds
x in X
let x be Element of L; :: thesis: ( x is completely-irreducible implies for X being Subset of L st ex_inf_of X,L & x = inf X holds
x in X )
assume x is completely-irreducible ; :: thesis: for X being Subset of L st ex_inf_of X,L & x = inf X holds
x in X
then consider q being Element of L such that
A1: x < q and
A2: for s being Element of L st x < s holds
q <= s and
uparrow x = {x} \/ (uparrow q) by Th20;
let X be Subset of L; :: thesis: ( ex_inf_of X,L & x = inf X implies x in X )
assume that
A3: ex_inf_of X,L and
A4: x = inf X and
A5: not x in X ; :: thesis: contradiction
A6: X c= uparrow q

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in uparrow q )
assume A7: y in X ; :: thesis: y in uparrow q
then reconsider y1 = y as Element of L ;
inf X is_<=_than X by A3, YELLOW_0:31;
then x <= y1 by A4, A7, LATTICE3:def 8;
then x < y1 by A5, A7, ORDERS_2:def 6;
then q <= y1 by A2;
hence y in uparrow q by WAYBEL_0:18; :: thesis: verum

end;

ex_inf_of uparrow q,L by WAYBEL_0:39;
then inf (uparrow q) <= inf X by A3, A6, YELLOW_0:35;
then q <= x by A4, WAYBEL_0:39;
hence contradiction by A1, ORDERS_2:6; :: thesis: verum