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

assume x in () ` ; :: thesis: ex y being Element of L st
( y in () ` & 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 ;
not y in downarrow l by ;
then y in () ` by XBOOLE_0:def 5;
hence ex y being Element of L st
( y in () ` & 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 = () ` 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 ;
l <= l ;
then l in F ` by WAYBEL_0:17;
hence l is_maximal_in F ` by ; :: 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;