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

now :: thesis: for b being Element of L st b in X holds
q <= b

let b be Element of L; :: thesis: ( b in X implies q <= b )
assume A7: b in X ; :: thesis: q <= b
then p <= b by A6, LATTICE3:def 8;
then p < b by A3, A7, ORDERS_2:def 6;
hence q <= b by A5; :: thesis: verum

end;

then A8: q is_<=_than X by LATTICE3:def 8;
A9: p <= q by A4, ORDERS_2:def 6;

now :: thesis: for b being Element of L st b is_<=_than X holds
q >= b

let b be Element of L; :: thesis: ( b is_<=_than X implies q >= b )
assume b is_<=_than X ; :: thesis: q >= b
then p >= b by A2, YELLOW_0:33;
hence q >= b by A9, ORDERS_2:3; :: thesis: verum

end;

hence contradiction by A2, A4, A8, YELLOW_0:33; :: thesis: verum