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 b₁ being Element of the carrier of L st
( b₁ in I ` & b<sub>1</sub> <= x & b<sub>1</sub> <= y ) )
assume ( x in I ` & y in I ` ) ; :: thesis: ex b<sub>1</sub> being Element of the carrier of L st
( b<sub>1</sub> in I ` & b₁ <= x & b₁ <= y )
then ( not x in I & not y in I ) by XBOOLE_0:def 5;
then A3: x "/\" y in I ` by A1, SUBSET_1:29;
( x "/\" y <= x & x "/\" y <= y ) by YELLOW_0:23;
hence ex b<sub>1</sub> being Element of the carrier of L st
( b<sub>1</sub> in I ` & b₁ <= x & b₁ <= 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 A5, WAYBEL_0:def 19;
hence y in I ` by A4, XBOOLE_0:def 5; :: 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 A6, WAYBEL_0:41;
hence ( x in I or y in I ) by SUBSET_1:29; :: thesis: verum