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 )

( 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

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

( not waybelow x is empty & waybelow x is directed ) ;

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;( 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 )

assume
l is prime
; :: thesis: ex F being Open Filter of L st l is_maximal_in F ` 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;( 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

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

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;

end;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

hence
l is prime
; :: thesis: verumy <= 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;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