let L be with_infima Poset; :: thesis: for I being Ideal of L holds
( I is prime iff for A being non empty finite Subset of L st inf A in I holds
ex a being Element of L st
( a in A & a in I ) )

let I be Ideal of L; :: thesis: ( I is prime iff for A being non empty finite Subset of L st inf A in I holds
ex a being Element of L st
( a in A & a in I ) )

thus ( I is prime implies for A being non empty finite Subset of L st inf A in I holds
ex a being Element of L st
( a in A & a in I ) ) :: thesis: ( ( for A being non empty finite Subset of L st inf A in I holds
ex a being Element of L st
( a in A & a in I ) ) implies I is prime )
proof
defpred S1[ set ] means ( not \$1 is empty & "/\" (\$1,L) in I implies ex a being Element of L st
( a in \$1 & a in I ) );
assume A1: for x, y being Element of L holds
( not x "/\" y in I or x in I or y in I ) ; :: according to WAYBEL_7:def 1 :: thesis: for A being non empty finite Subset of L st inf A in I holds
ex a being Element of L st
( a in A & a in I )

let A be non empty finite Subset of L; :: thesis: ( inf A in I implies ex a being Element of L st
( a in A & a in I ) )

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: "/\" ((B \/ {x}),L) in I ; :: thesis: ex a being Element of L st
( a in B \/ {x} & a in I )

per cases ( B = {} or B <> {} ) ;
suppose B = {} ; :: thesis: ex a being Element of L st
( a in B \/ {x} & a in I )

then ( "/\" ((B \/ {a}),L) = a & a in B \/ {a} ) by ;
hence ex a being Element of L st
( a in B \/ {x} & a in I ) by A6; :: thesis: verum
end;
suppose A7: B <> {} ; :: thesis: ex a being Element of L st
( a in B \/ {x} & a in I )

A8: inf {a} = a by YELLOW_0:39;
A9: ex_inf_of {a},L by YELLOW_0:55;
ex_inf_of C,L by ;
then A10: "/\" ((B \/ {x}),L) = (inf C) "/\" () by ;
hereby :: thesis: verum
per cases ( inf C in I or a in I ) by A1, A6, A10, A8;
suppose inf C in I ; :: thesis: ex b being Element of L st
( b in B \/ {x} & b in I )

then consider b being Element of L such that
A11: ( b in B & b in I ) by A5, A7;
take b = b; :: thesis: ( b in B \/ {x} & b in I )
thus ( b in B \/ {x} & b in I ) by ; :: thesis: verum
end;
suppose A12: a in I ; :: thesis: ex a being Element of L st
( a in B \/ {x} & a in I )

take a = a; :: thesis: ( a in B \/ {x} & a in I )
a in {a} by TARSKI:def 1;
hence ( a in B \/ {x} & a in I ) 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 ( inf A in I implies ex a being Element of L st
( a in A & a in I ) ) ; :: thesis: verum
end;
assume A15: for A being non empty finite Subset of L st inf A in I holds
ex a being Element of L st
( a in A & a in I ) ; :: thesis: I is prime
let a, b be Element of L; :: according to WAYBEL_7:def 1 :: thesis: ( not a "/\" b in I or a in I or b in I )
assume a "/\" b in I ; :: thesis: ( a in I or b in I )
then inf {a,b} in I by YELLOW_0:40;
then ex x being Element of L st
( x in {a,b} & x in I ) by A15;
hence ( a in I or b in I ) by TARSKI:def 2; :: thesis: verum