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 )

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

( 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

assume A15:
for A being non empty finite Subset of L st I = inf A holds
defpred S_{1}[ 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 )

_{1}[ {} ]
;

A14: A is finite ;

S_{1}[A]
from FINSET_1:sch 2(A14, A13, A2);

hence ( I = inf A implies I in A ) ; :: thesis: verum

end;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 & S_{1}[B] holds

S_{1}[B \/ {x}]

A13:
SS

let x, B be set ; :: thesis: ( x in A & B c= A & S_{1}[B] implies S_{1}[B \/ {x}] )

assume that

A3: x in A and

A4: B c= A and

A5: S_{1}[B]
; :: thesis: S_{1}[B \/ {x}]

thus S_{1}[B \/ {x}]
:: thesis: verum

end;assume that

A3: x in A and

A4: B c= A and

A5: S

thus S

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: I in B \/ {x}

end;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: I in B \/ {x}

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

end;

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

then
"/\" ((B \/ {a}),L) = a
by YELLOW_0:39;

hence I in B \/ {x} by A6, A7, TARSKI:def 1; :: thesis: verum

end;hence I in B \/ {x} by A6, A7, TARSKI:def 1; :: thesis: verum

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 A8, YELLOW_0:55;

then A11: "/\" ((B \/ {x}),L) = (inf C) "/\" (inf {a}) by A10, YELLOW_2:4;

end;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;

A14: A is finite ;

S

hence ( I = inf A implies I in A ) ; :: thesis: verum

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