let L be Semilattice; :: thesis: for x being Element of L holds
( x is meet-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 meet-irreducible iff for A being non empty finite Subset of L st I = inf A holds
I in A )
thus ( I is meet-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 meet-irreducible )

proof

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: A is finite ;
defpred S₁[ set ] means ( not $1 is empty & I = "/\" $1,L implies I in $1 );
A3: S₁[ {} ] ;

A4: now

let x, B be set ; :: thesis: ( x in A & B c= A & S₁[B] implies S₁[B \/ {x}] )
assume that
A5: ( x in A & B c= A ) and
A6: S₁[B] ; :: thesis: S₁[B \/ {x}]
thus S₁[B \/ {x}] :: thesis: verum

proof

assume A7: ( not B \/ {x} is empty & I = "/\" (B \/ {x}),L ) ; :: thesis: I in B \/ {x}
reconsider C = B as finite Subset of L by A5, XBOOLE_1:1;
reconsider a = x as Element of L by A5;

per cases ( B = {} or B <> {} ) ;

suppose B = {} ; :: thesis: I in B \/ {x}

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

end;

suppose A8: B <> {} ; :: thesis: I in B \/ {x}

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

hereby :: thesis: verum

per cases ( inf C = I or a = I ) by A1, A7, A9;

suppose inf C = I ; :: thesis: I in B \/ {x}

then consider b being Element of L such that
A10: ( b in B & b = I ) by A6, A8;
thus I in B \/ {x} by A10, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A11: a = I ; :: thesis: I in B \/ {x}

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

end;

end;

end;

end;

end;

end;

end;

S₁[A] from FINSET_1:sch 2(A2, A3, A4);
hence ( I = inf A implies I in A ) ; :: thesis: verum

end;

assume A12: for A being non empty finite Subset of L st I = inf A holds
I in A ; :: thesis: I is meet-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 A12;
hence ( a = I or b = I ) by TARSKI:def 2; :: thesis: verum