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 )

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

( 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 A6:
( I ` is Filter of L or I ` = {} )
; :: thesis: I is prime
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

end;( 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

I ` is upper
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_{1} being Element of the carrier of L st

( b_{1} in I ` & b_{1} <= x & b_{1} <= y ) )

assume ( x in I ` & y in I ` ) ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in I ` & b_{1} <= x & b_{1} <= 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_{1} being Element of the carrier of L st

( b_{1} in I ` & b_{1} <= x & b_{1} <= y )
by A3; :: thesis: verum

end;( b

assume ( x in I ` & y in I ` ) ; :: thesis: ex b

( b

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

( b

proof

hence
( I ` is Filter of L or I ` = {} )
by A2; :: thesis: verum
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;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

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