let L be Semilattice; :: thesis:
let I be Element of L; :: thesis:
thus ( I is irreducible implies for A being non empty finite Subset of L st I = inf A holds
I in A ) :: thesis:

proof

defpred S₁[ set ] means ( not $1 is empty & I = "/\" ($1,L) implies I in $1 );
assume A1: for x, y being Element of L holds
( not I = x "/\" y or I = x or I = y ) ; :: according to WAYBEL_6:def 2 :: thesis:
let A be non empty finite Subset of L; :: thesis:

A2: now :: thesis:

let x, B be set ; :: thesis:
assume that
A3: x in A and
A4: B c= A and
A5: S₁[B] ; :: thesis:
thus S₁[B \/ {x}] :: thesis:

proof

reconsider a = x as Element of L by A3;
reconsider C = B as finite Subset of L by A4, XBOOLE_1:1;
assume that
not B \/ {x} is empty and
A6: I = "/\" ((B \/ {x}),L) ; :: thesis:

per cases ;

suppose A7: B = {} ; :: thesis:

then "/\" ((B \/ {a}),L) = a by YELLOW_0:39;
hence I in B \/ {x} by A6, A7, TARSKI:def 1; :: thesis:

end;

suppose A8: B <> {} ; :: thesis:

A9: inf {a} = a by YELLOW_0:39;
A10: ex_inf_of {a},L by YELLOW_0:55;
ex_inf_of C,L by A8, YELLOW_0:55;
then A11: "/\" ((B \/ {x}),L) = (inf C) "/\" (inf {a}) by A10, YELLOW_2:4;

hereby :: thesis:

per cases by A1, A6, A11, A9;

suppose inf C = I ; :: thesis:

hence I in B \/ {x} by A5, A8, XBOOLE_0:def 3; :: thesis:

end;

suppose A12: a = I ; :: thesis:

a in {a} by TARSKI:def 1;
hence I in B \/ {x} by A12, XBOOLE_0:def 3; :: thesis:

end;

end;

end;

end;

end;

end;

end;

A13: S₁[ {} ] ;
A14: A is finite ;
S₁[A] from FINSET_1:sch 2(A14, A13, A2);
hence ( I = inf A implies I in A ) ; :: thesis:

end;

assume A15: for A being non empty finite Subset of L st I = inf A holds
I in A ; :: thesis:
let a, b be Element of L; :: according to WAYBEL_6:def 2 :: thesis:
assume I = a "/\" b ; :: thesis:
then I = inf {a,b} by YELLOW_0:40;
then I in {a,b} by A15;
hence ( a = I or b = I ) by TARSKI:def 2; :: thesis: