let L be lower-bounded distributive continuous LATTICE; :: thesis:
let l be Element of L; :: thesis:
set F = (downarrow l) ` ;
assume A1: l <> Top L ; :: thesis:
thus ( l is prime implies ex F being Open Filter of L st l is_maximal_in F ` ) :: thesis:

A2: for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ;

A3: now :: thesis:

let x be Element of L; :: thesis:
assume x in (downarrow l) ` ; :: thesis:
then not x in downarrow l by XBOOLE_0:def 5;
then not x <= l by WAYBEL_0:17;
then consider y being Element of L such that
A4: y << x and
A5: not y <= l by A2, WAYBEL_3:24;
not y in downarrow l by A5, WAYBEL_0:17;
then y in (downarrow l) ` by XBOOLE_0:def 5;
hence ex y being Element of L st
( y in (downarrow l) ` & y << x ) by A4; :: thesis:

end;

assume l is prime ; :: thesis:
then reconsider F = (downarrow l) ` as Open Filter of L by A1, A3, Def1, Th26;
take F ; :: thesis:
A6: for y being Element of L holds
( not y in F ` or not y > l ) by WAYBEL_0:17, ORDERS_2:6;
l <= l ;
then l in F ` by WAYBEL_0:17;
hence l is_maximal_in F ` by A6, WAYBEL_4:55; :: thesis:

end;

thus ( ex F being Open Filter of L st l is_maximal_in F ` implies l is prime ) :: thesis:

assume ex O being Open Filter of L st l is_maximal_in O ` ; :: thesis:
then A7: l is irreducible by Th13;

let x, y be Element of L; :: thesis:
assume x "/\" y <= l ; :: thesis:
then l = l "\/" (x "/\" y) by YELLOW_0:24
.= (l "\/" x) "/\" (l "\/" y) by WAYBEL_1:5 ;
then A8: ( l = l "\/" x or l = l "\/" y ) by A7;
assume ( not x <= l & not y <= l ) ; :: thesis:
hence contradiction by A8, YELLOW_0:24; :: thesis:

end;

hence l is prime ; :: thesis:

end;