let L be with_infima Poset; :: thesis: for I being Ideal of L holds
( I is prime iff ( I ` is Filter of L or I ` = {} ) )

let I be Ideal of L; :: thesis: ( I is prime iff ( I ` is Filter of L or I ` = {} ) )
set F = I ` ;
thus ( not I is prime or I ` is Filter of L or I ` = {} ) :: thesis: ( ( I ` is Filter of L or I ` = {} ) implies I is prime )
proof
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: ( I ` is Filter of L or I ` = {} )
A2: I ` is filtered
proof
let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( not x in I ` or not y in I ` or ex b1 being Element of the carrier of L st
( b1 in I ` & b1 <= x & b1 <= y ) )

assume ( x in I ` & y in I ` ) ; :: thesis: ex b1 being Element of the carrier of L st
( b1 in I ` & b1 <= x & b1 <= y )

then ( not x in I & not y in I ) by XBOOLE_0:def 5;
then A3: x "/\" y in I ` by ;
( x "/\" y <= x & x "/\" y <= y ) by YELLOW_0:23;
hence ex b1 being Element of the carrier of L st
( b1 in I ` & b1 <= x & b1 <= y ) by A3; :: thesis: verum
end;
I ` is upper
proof
let x, y be Element of L; :: according to WAYBEL_0:def 20 :: thesis: ( not x in I ` or not x <= y or y in I ` )
assume that
A4: x in I ` and
A5: y >= x ; :: thesis: y in I `
( y in I implies x in I ) by ;
hence y in I ` by ; :: thesis: verum
end;
hence ( I ` is Filter of L or I ` = {} ) by A2; :: thesis: verum
end;
assume A6: ( I ` is Filter of L or I ` = {} ) ; :: thesis: I is prime
let x, y be Element of L; :: according to WAYBEL_7:def 1 :: thesis: ( not x "/\" y in I or x in I or y in I )
assume x "/\" y in I ; :: thesis: ( x in I or y in I )
then not x "/\" y in I ` by XBOOLE_0:def 5;
then ( not x in I ` or not y in I ` ) by ;
hence ( x in I or y in I ) by SUBSET_1:29; :: thesis: verum