let L be upper-bounded LATTICE; :: thesis: for l being Element of L st l <> Top L holds
( l is prime iff () ` is Filter of L )

let l be Element of L; :: thesis: ( l <> Top L implies ( l is prime iff () ` is Filter of L ) )
set X1 = the carrier of L \ ();
reconsider X = the carrier of L \ () as Subset of L ;
assume A1: l <> Top L ; :: thesis: ( l is prime iff () ` is Filter of L )
thus ( l is prime implies () ` is Filter of L ) :: thesis: ( () ` is Filter of L implies l is prime )
proof
assume A2: l is prime ; :: thesis: () ` is Filter of L
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 )
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 ;
then A6: not y <= l by WAYBEL_0:17;
not x in downarrow l by ;
then A7: not x <= l by WAYBEL_0:17;
not x "/\" y in downarrow l by ;
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;
A9: now :: thesis: for x, y being Element of L st x in X & x <= y holds
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 ;
then not x <= l by WAYBEL_0:17;
then not y <= l by ;
then not y in downarrow l by WAYBEL_0:17;
hence y in X by XBOOLE_0:def 5; :: thesis: verum
end;
now :: thesis: not Top L in downarrow lend;
hence (downarrow l) ` is Filter of L by ; :: thesis: verum
end;
thus ( (downarrow l) ` is Filter of L implies l is prime ) :: 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 )
now :: thesis: ( not x <= l implies y <= l )
assume that
A15: not x <= l and
A16: not y <= l ; :: thesis: contradiction
not y in downarrow l by ;
then A17: y in X by XBOOLE_0:def 5;
not x in downarrow l by ;
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 ;
z <= x "/\" y by ;
then z <= l by ;
then l in X by ;
hence contradiction by A12, XBOOLE_0:def 5; :: thesis: verum
end;
hence ( x <= l or y <= l ) ; :: thesis: verum
end;