let L be Semilattice; :: thesis: for l being Element of L holds

( l is prime iff for A being non empty finite Subset of L st l >= inf A holds

ex a being Element of L st

( a in A & l >= a ) )

let l be Element of L; :: thesis: ( l is prime iff for A being non empty finite Subset of L st l >= inf A holds

ex a being Element of L st

( a in A & l >= a ) )

thus ( l is prime implies for A being non empty finite Subset of L st l >= inf A holds

ex a being Element of L st

( a in A & l >= a ) ) :: thesis: ( ( for A being non empty finite Subset of L st l >= inf A holds

ex a being Element of L st

( a in A & l >= a ) ) implies l is prime )

ex a being Element of L st

( a in A & l >= a ) ; :: thesis: l is prime

let a, b be Element of L; :: according to WAYBEL_6:def 6 :: thesis: ( not a "/\" b <= l or a <= l or b <= l )

set A = {a,b};

A17: inf {a,b} = a "/\" b by YELLOW_0:40;

assume a "/\" b <= l ; :: thesis: ( a <= l or b <= l )

then ex k being Element of L st

( k in {a,b} & l >= k ) by A16, A17;

hence ( a <= l or b <= l ) by TARSKI:def 2; :: thesis: verum

( l is prime iff for A being non empty finite Subset of L st l >= inf A holds

ex a being Element of L st

( a in A & l >= a ) )

let l be Element of L; :: thesis: ( l is prime iff for A being non empty finite Subset of L st l >= inf A holds

ex a being Element of L st

( a in A & l >= a ) )

thus ( l is prime implies for A being non empty finite Subset of L st l >= inf A holds

ex a being Element of L st

( a in A & l >= a ) ) :: thesis: ( ( for A being non empty finite Subset of L st l >= inf A holds

ex a being Element of L st

( a in A & l >= a ) ) implies l is prime )

proof

assume A16:
for A being non empty finite Subset of L st l >= inf A holds
defpred S_{1}[ set ] means ( not $1 is empty & l >= "/\" ($1,L) implies ex k being Element of L st

( k in $1 & l >= k ) );

assume A1: for x, y being Element of L holds

( not l >= x "/\" y or l >= x or l >= y ) ; :: according to WAYBEL_6:def 6 :: thesis: for A being non empty finite Subset of L st l >= inf A holds

ex a being Element of L st

( a in A & l >= a )

let A be non empty finite Subset of L; :: thesis: ( l >= inf A implies ex a being Element of L st

( a in A & l >= a ) )

_{1}[ {} ]
;

A15: A is finite ;

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

hence ( l >= inf A implies ex a being Element of L st

( a in A & l >= a ) ) ; :: thesis: verum

end;( k in $1 & l >= k ) );

assume A1: for x, y being Element of L holds

( not l >= x "/\" y or l >= x or l >= y ) ; :: according to WAYBEL_6:def 6 :: thesis: for A being non empty finite Subset of L st l >= inf A holds

ex a being Element of L st

( a in A & l >= a )

let A be non empty finite Subset of L; :: thesis: ( l >= inf A implies ex a being Element of L st

( a in A & l >= a ) )

A2: now :: thesis: for x, B being set st x in A & B c= A & S_{1}[B] holds

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

A14:
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: l >= "/\" ((B \/ {x}),L) ; :: thesis: ex k being Element of L st

( k in B \/ {x} & l >= k )

end;reconsider C = B as finite Subset of L by A4, XBOOLE_1:1;

assume that

not B \/ {x} is empty and

A6: l >= "/\" ((B \/ {x}),L) ; :: thesis: ex k being Element of L st

( k in B \/ {x} & l >= k )

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

end;

suppose
B = {}
; :: thesis: ex k being Element of L st

( k in B \/ {x} & l >= k )

( k in B \/ {x} & l >= k )

then
( "/\" ((B \/ {a}),L) = a & a in B \/ {a} )
by TARSKI:def 1, YELLOW_0:39;

hence ex k being Element of L st

( k in B \/ {x} & l >= k ) by A6; :: thesis: verum

end;hence ex k being Element of L st

( k in B \/ {x} & l >= k ) by A6; :: thesis: verum

suppose A7:
B <> {}
; :: thesis: ex k being Element of L st

( k in B \/ {x} & l >= k )

( k in B \/ {x} & l >= k )

A8:
inf {a} = a
by YELLOW_0:39;

A9: ex_inf_of {a},L by YELLOW_0:55;

ex_inf_of C,L by A7, YELLOW_0:55;

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

end;A9: ex_inf_of {a},L by YELLOW_0:55;

ex_inf_of C,L by A7, YELLOW_0:55;

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

hereby :: thesis: verum
end;

per cases
( inf C <= l or a <= l )
by A1, A6, A10, A8;

end;

A15: A is finite ;

S

hence ( l >= inf A implies ex a being Element of L st

( a in A & l >= a ) ) ; :: thesis: verum

ex a being Element of L st

( a in A & l >= a ) ; :: thesis: l is prime

let a, b be Element of L; :: according to WAYBEL_6:def 6 :: thesis: ( not a "/\" b <= l or a <= l or b <= l )

set A = {a,b};

A17: inf {a,b} = a "/\" b by YELLOW_0:40;

assume a "/\" b <= l ; :: thesis: ( a <= l or b <= l )

then ex k being Element of L st

( k in {a,b} & l >= k ) by A16, A17;

hence ( a <= l or b <= l ) by TARSKI:def 2; :: thesis: verum