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 )
proof
defpred S1[ 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 ) )
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 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 <> {} ) ;
suppose B = {} ; :: thesis: ex k being Element of L st
( 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;
suppose A7: B <> {} ; :: thesis: ex k being Element of L st
( 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;
hereby :: thesis: verum
per cases ( inf C <= l or a <= l ) by A1, A6, A10, A8;
suppose inf C <= l ; :: thesis: ex k being Element of L st
( k in B \/ {x} & l >= k )
then consider b being Element of L such that
A11: b in B and
A12: b <= l by A5, A7;
b in B \/ {x} by A11, XBOOLE_0:def 3;
hence ex k being Element of L st
( k in B \/ {x} & l >= k ) by A12; :: thesis: verum
end;
suppose A13: a <= l ; :: thesis: ex k being Element of L st
( k in B \/ {x} & l >= k )
a in {a} by TARSKI:def 1;
then a in B \/ {x} by XBOOLE_0:def 3;
hence ex k being Element of L st
( k in B \/ {x} & l >= k ) by A13; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
A14: S1[ {} ] ;
A15: A is finite ;
S1[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;
assume A16: 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: 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