let L be upper-bounded LATTICE; :: thesis: for l being Element of L st l <> Top L holds

( l is prime iff (downarrow l) ` is Filter of L )

let l be Element of L; :: thesis: ( l <> Top L implies ( l is prime iff (downarrow l) ` is Filter of L ) )

set X1 = the carrier of L \ (downarrow l);

reconsider X = the carrier of L \ (downarrow l) as Subset of L ;

assume A1: l <> Top L ; :: thesis: ( l is prime iff (downarrow l) ` is Filter of L )

thus ( l is prime implies (downarrow l) ` is Filter of L ) :: thesis: ( (downarrow l) ` is Filter of L implies l is prime )

( l is prime iff (downarrow l) ` is Filter of L )

let l be Element of L; :: thesis: ( l <> Top L implies ( l is prime iff (downarrow l) ` is Filter of L ) )

set X1 = the carrier of L \ (downarrow l);

reconsider X = the carrier of L \ (downarrow l) as Subset of L ;

assume A1: l <> Top L ; :: thesis: ( l is prime iff (downarrow l) ` is Filter of L )

thus ( l is prime implies (downarrow l) ` is Filter of L ) :: thesis: ( (downarrow l) ` is Filter of L implies l is prime )

proof

thus
( (downarrow l) ` is Filter of L implies l is prime )
:: thesis: verum
assume A2:
l is prime
; :: thesis: (downarrow l) ` is Filter of L

end;A3: now :: thesis: for x, y being Element of L st x in X & y in X holds

ex z being Element of L st

( z in X & z <= x & z <= y )

ex z being Element of L st

( z in X & z <= x & z <= y )

let x, y be Element of L; :: thesis: ( x in X & y in X implies ex z being Element of L st

( z in X & z <= x & z <= y ) )

assume that

A4: x in X and

A5: y in X ; :: thesis: ex z being Element of L st

( z in X & z <= x & z <= y )

not y in downarrow l by A5, XBOOLE_0:def 5;

then A6: not y <= l by WAYBEL_0:17;

not x in downarrow l by A4, XBOOLE_0:def 5;

then A7: not x <= l by WAYBEL_0:17;

not x "/\" y in downarrow l by A2, A7, A6, WAYBEL_0:17;

then A8: x "/\" y in X by XBOOLE_0:def 5;

( x "/\" y <= x & x "/\" y <= y ) by YELLOW_0:23;

hence ex z being Element of L st

( z in X & z <= x & z <= y ) by A8; :: thesis: verum

end;( z in X & z <= x & z <= y ) )

assume that

A4: x in X and

A5: y in X ; :: thesis: ex z being Element of L st

( z in X & z <= x & z <= y )

not y in downarrow l by A5, XBOOLE_0:def 5;

then A6: not y <= l by WAYBEL_0:17;

not x in downarrow l by A4, XBOOLE_0:def 5;

then A7: not x <= l by WAYBEL_0:17;

not x "/\" y in downarrow l by A2, A7, A6, WAYBEL_0:17;

then A8: x "/\" y in X by XBOOLE_0:def 5;

( x "/\" y <= x & x "/\" y <= y ) by YELLOW_0:23;

hence ex z being Element of L st

( z in X & z <= x & z <= y ) by A8; :: thesis: verum

A9: now :: thesis: for x, y being Element of L st x in X & x <= y holds

y in X

y in X

let x, y be Element of L; :: thesis: ( x in X & x <= y implies y in X )

assume that

A10: x in X and

A11: x <= y ; :: thesis: y in X

not x in downarrow l by A10, XBOOLE_0:def 5;

then not x <= l by WAYBEL_0:17;

then not y <= l by A11, ORDERS_2:3;

then not y in downarrow l by WAYBEL_0:17;

hence y in X by XBOOLE_0:def 5; :: thesis: verum

end;assume that

A10: x in X and

A11: x <= y ; :: thesis: y in X

not x in downarrow l by A10, XBOOLE_0:def 5;

then not x <= l by WAYBEL_0:17;

then not y <= l by A11, ORDERS_2:3;

then not y in downarrow l by WAYBEL_0:17;

hence y in X by XBOOLE_0:def 5; :: thesis: verum

now :: thesis: not Top L in downarrow l

hence
(downarrow l) ` is Filter of L
by A3, A9, WAYBEL_0:def 2, WAYBEL_0:def 20, XBOOLE_0:def 5; :: thesis: verumassume
Top L in downarrow l
; :: thesis: contradiction

then Top L <= l by WAYBEL_0:17;

then Top L < l by A1, ORDERS_2:def 6;

hence contradiction by ORDERS_2:6, YELLOW_0:45; :: thesis: verum

end;then Top L <= l by WAYBEL_0:17;

then Top L < l by A1, ORDERS_2:def 6;

hence contradiction by ORDERS_2:6, YELLOW_0:45; :: thesis: verum

proof

l <= l
;

then A12: l in downarrow l by WAYBEL_0:17;

assume A13: (downarrow l) ` is Filter of L ; :: thesis: l is prime

let x, y be Element of L; :: according to WAYBEL_6:def 6 :: thesis: ( not x "/\" y <= l or x <= l or y <= l )

assume A14: x "/\" y <= l ; :: thesis: ( x <= l or y <= l )

end;then A12: l in downarrow l by WAYBEL_0:17;

assume A13: (downarrow l) ` is Filter of L ; :: thesis: l is prime

let x, y be Element of L; :: according to WAYBEL_6:def 6 :: thesis: ( not x "/\" y <= l or x <= l or y <= l )

assume A14: x "/\" y <= l ; :: thesis: ( x <= l or y <= l )

now :: thesis: ( not x <= l implies y <= l )

hence
( x <= l or y <= l )
; :: thesis: verumassume that

A15: not x <= l and

A16: not y <= l ; :: thesis: contradiction

not y in downarrow l by A16, WAYBEL_0:17;

then A17: y in X by XBOOLE_0:def 5;

not x in downarrow l by A15, WAYBEL_0:17;

then x in X by XBOOLE_0:def 5;

then consider z being Element of L such that

A18: z in X and

A19: ( z <= x & z <= y ) by A13, A17, WAYBEL_0:def 2;

z <= x "/\" y by A19, YELLOW_0:23;

then z <= l by A14, ORDERS_2:3;

then l in X by A13, A18, WAYBEL_0:def 20;

hence contradiction by A12, XBOOLE_0:def 5; :: thesis: verum

end;A15: not x <= l and

A16: not y <= l ; :: thesis: contradiction

not y in downarrow l by A16, WAYBEL_0:17;

then A17: y in X by XBOOLE_0:def 5;

not x in downarrow l by A15, WAYBEL_0:17;

then x in X by XBOOLE_0:def 5;

then consider z being Element of L such that

A18: z in X and

A19: ( z <= x & z <= y ) by A13, A17, WAYBEL_0:def 2;

z <= x "/\" y by A19, YELLOW_0:23;

then z <= l by A14, ORDERS_2:3;

then l in X by A13, A18, WAYBEL_0:def 20;

hence contradiction by A12, XBOOLE_0:def 5; :: thesis: verum