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

proof

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

A3: now :: thesis: for x being Element of L st x in (downarrow l) ` holds
ex y being Element of L st
( y in (downarrow l) ` & y << x )

let x be Element of L; :: thesis: ( x in (downarrow l) ` implies ex y being Element of L st
( y in (downarrow l) ` & y << x ) )
assume x in (downarrow l) ` ; :: thesis: ex y being Element of L st
( y in (downarrow l) ` & y << x )
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: verum

end;

assume l is prime ; :: thesis: ex F being Open Filter of L st l is_maximal_in F `
then reconsider F = (downarrow l) ` as Open Filter of L by A1, A3, Def1, Th26;
take F ; :: thesis: l is_maximal_in F `
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: verum

end;

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

proof

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

now :: thesis: for x, y being Element of L st x "/\" y <= l & not x <= l holds
y <= l

let x, y be Element of L; :: thesis: ( x "/\" y <= l & not x <= l implies y <= l )
assume x "/\" y <= l ; :: thesis: ( not x <= l implies y <= l )
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: contradiction
hence contradiction by A8, YELLOW_0:24; :: thesis: verum

end;

hence l is prime ; :: thesis: verum

end;