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

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

thus ( I is irreducible implies for A being non empty finite Subset of L st I = inf A holds
I in A ) :: thesis: ( ( for A being non empty finite Subset of L st I = inf A holds
I in A ) implies I is irreducible )
proof
defpred S1[ 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: for A being non empty finite Subset of L st I = inf A holds
I in A

let A be non empty finite Subset of L; :: thesis: ( I = inf A implies I in A )
A2: now :: thesis: for x, B being set st x in A & B c= A & S1[B] holds
S1[B \/ {x}]
let x, B be set ; :: thesis: ( x in A & B c= A & S1[B] implies S1[B \/ {x}] )
assume that
A3: x in A and
A4: B c= A and
A5: S1[B] ; :: thesis: S1[B \/ {x}]
thus S1[B \/ {x}] :: thesis: verum
proof
reconsider a = x as Element of L by A3;
reconsider C = B as finite Subset of L by ;
assume that
not B \/ {x} is empty and
A6: I = "/\" ((B \/ {x}),L) ; :: thesis: I in B \/ {x}
per cases ( B = {} or B <> {} ) ;
suppose A7: B = {} ; :: thesis: I in B \/ {x}
then "/\" ((B \/ {a}),L) = a by YELLOW_0:39;
hence I in B \/ {x} by ; :: thesis: verum
end;
suppose A8: B <> {} ; :: thesis: I in B \/ {x}
A9: inf {a} = a by YELLOW_0:39;
A10: ex_inf_of {a},L by YELLOW_0:55;
ex_inf_of C,L by ;
then A11: "/\" ((B \/ {x}),L) = (inf C) "/\" () by ;
hereby :: thesis: verum
per cases ( inf C = I or a = I ) by A1, A6, A11, A9;
suppose inf C = I ; :: thesis: I in B \/ {x}
hence I in B \/ {x} by ; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
A13: S1[ {} ] ;
A14: A is finite ;
S1[A] from FINSET_1:sch 2(A14, A13, A2);
hence ( I = inf A implies I in A ) ; :: thesis: verum
end;
assume A15: for A being non empty finite Subset of L st I = inf A holds
I in A ; :: thesis: I is irreducible
let a, b be Element of L; :: according to WAYBEL_6:def 2 :: thesis: ( not I = a "/\" b or a = I or b = I )
assume I = a "/\" b ; :: thesis: ( a = I or b = I )
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: verum