let L be Semilattice; :: thesis: Irr L c= IRR L
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Irr L or x in IRR L )
assume A1: x in Irr L ; :: thesis: x in IRR L
then reconsider x1 = x as Element of L ;
x1 is completely-irreducible by A1, Def4;
then consider q being Element of L such that
A2: x1 < q and
A3: for s being Element of L st x1 < s holds
q <= s and
uparrow x1 = {x1} \/ (uparrow q) by Th20;

now :: thesis: for a, b being Element of L st x1 = a "/\" b & a <> x1 holds
not b <> x1

let a, b be Element of L; :: thesis: ( x1 = a "/\" b & a <> x1 implies not b <> x1 )
assume that
A4: x1 = a "/\" b and
A5: a <> x1 and
A6: b <> x1 ; :: thesis: contradiction
x1 <= b by A4, YELLOW_0:23;
then x1 < b by A6, ORDERS_2:def 6;
then A7: q <= b by A3;
A8: x1 <= q by A2, ORDERS_2:def 6;
x1 <= a by A4, YELLOW_0:23;
then x1 < a by A5, ORDERS_2:def 6;
then q <= a by A3;
then q <= x1 by A4, A7, YELLOW_0:23;
hence contradiction by A2, A8, ORDERS_2:2; :: thesis: verum

end;

then x1 is irreducible by WAYBEL_6:def 2;
hence x in IRR L by WAYBEL_6:def 4; :: thesis: verum