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 ` ) )
assume A1: l <> Top L ; :: thesis: ( l is prime iff ex F being Open Filter of L st l is_maximal_in F ` )
set F = (downarrow l) ` ;
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

assume A2: l is prime ; :: thesis: ex F being Open Filter of L st l is_maximal_in F `
A3: ( ( for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ) & L is up-complete & L is satisfying_axiom_of_approximation ) ;

now

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 & not y <= l ) by A3, WAYBEL_3:24;
not y in downarrow l by A4, 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;

then reconsider F = (downarrow l) ` as Open Filter of L by A1, A2, Def1, Th26;
take F ; :: thesis: l is_maximal_in F `
l <= l ;
then A5: l in F ` by WAYBEL_0:17;

now

given y being Element of L such that A6: ( y in F ` & y > l ) ; :: thesis: contradiction
y <= l by A6, WAYBEL_0:17;
hence contradiction by A6, ORDERS_2:30; :: thesis: verum

end;

hence l is_maximal_in F ` by A5, WAYBEL_4:56; :: 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 meet-irreducible by Th13;

now

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

end;

hence l is prime by Def6; :: thesis: verum

end;