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 ) )
assume A1: l <> Top L ; :: thesis: ( 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 ;
thus ( l is prime implies (downarrow l) ` is Filter of L ) :: thesis: ( (downarrow l) ` is Filter of L implies l is prime )

proof

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

A3: now

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 ( x in X & y in X ) ; :: thesis: ex z being Element of L st
( z in X & z <= x & z <= y )
then ( x in the carrier of L & not x in downarrow l & y in the carrier of L & not y in downarrow l ) by XBOOLE_0:def 5;
then A4: ( not x <= l & not y <= l ) by WAYBEL_0:17;
A5: ( x "/\" y <= x & x "/\" y <= y ) by YELLOW_0:23;

now

assume x "/\" y in downarrow l ; :: thesis: contradiction
then x "/\" y <= l by WAYBEL_0:17;
hence contradiction by A2, A4, Def6; :: thesis: verum

end;

then x "/\" y in X by XBOOLE_0:def 5;
hence ex z being Element of L st
( z in X & z <= x & z <= y ) by A5; :: thesis: verum

end;

A6: now

let x, y be Element of L; :: thesis: ( x in X & x <= y implies y in X )
assume A7: ( x in X & x <= y ) ; :: thesis: y in X
then ( x in the carrier of L & not x in downarrow l ) by XBOOLE_0:def 5;
then not x <= l by WAYBEL_0:17;
then not y <= l by A7, ORDERS_2:26;
then not y in downarrow l by WAYBEL_0:17;
hence y in X by XBOOLE_0:def 5; :: thesis: verum

end;

now

assume Top L in downarrow l ; :: thesis: contradiction
then Top L <= l by WAYBEL_0:17;
then Top L < l by A1, ORDERS_2:def 10;
hence contradiction by ORDERS_2:30, YELLOW_0:45; :: thesis: verum

end;

hence (downarrow l) ` is Filter of L by A3, A6, WAYBEL_0:def 2, WAYBEL_0:def 20, XBOOLE_0:def 5; :: thesis: verum

end;

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

proof

assume A8: (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 A9: x "/\" y <= l ; :: thesis: ( x <= l or y <= l )
l <= l ;
then A10: l in downarrow l by WAYBEL_0:17;

now

assume ( not x <= l & not y <= l ) ; :: thesis: contradiction
then ( not x in downarrow l & not y in downarrow l ) by WAYBEL_0:17;
then ( x in X & y in X ) by XBOOLE_0:def 5;
then consider z being Element of L such that
A11: ( z in X & z <= x & z <= y ) by A8, WAYBEL_0:def 2;
z <= x "/\" y by A11, YELLOW_0:23;
then z <= l by A9, ORDERS_2:26;
then l in X by A8, A11, WAYBEL_0:def 20;
hence contradiction by A10, XBOOLE_0:def 5; :: thesis: verum

end;

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

end;