let L be Lattice; :: thesis: for F being Filter of L

for p, q being Element of L st p in <.(<.q.) \/ F).) holds

ex r being Element of L st

( r in F & q "/\" r [= p )

let F be Filter of L; :: thesis: for p, q being Element of L st p in <.(<.q.) \/ F).) holds

ex r being Element of L st

( r in F & q "/\" r [= p )

let p, q be Element of L; :: thesis: ( p in <.(<.q.) \/ F).) implies ex r being Element of L st

( r in F & q "/\" r [= p ) )

A1: <.(<.q.) \/ F).) = { r where r is Element of L : ex p9, q9 being Element of L st

( p9 "/\" q9 [= r & p9 in <.q.) & q9 in F ) } by FILTER_0:35;

assume p in <.(<.q.) \/ F).) ; :: thesis: ex r being Element of L st

( r in F & q "/\" r [= p )

then ex r being Element of L st

( r = p & ex p9, q9 being Element of L st

( p9 "/\" q9 [= r & p9 in <.q.) & q9 in F ) ) by A1;

then consider p9, q9 being Element of L such that

A2: p9 "/\" q9 [= p and

A3: p9 in <.q.) and

A4: q9 in F ;

q [= p9 by A3, FILTER_0:15;

then q "/\" q9 [= p9 "/\" q9 by LATTICES:9;

hence ex r being Element of L st

( r in F & q "/\" r [= p ) by A2, A4, LATTICES:7; :: thesis: verum

for p, q being Element of L st p in <.(<.q.) \/ F).) holds

ex r being Element of L st

( r in F & q "/\" r [= p )

let F be Filter of L; :: thesis: for p, q being Element of L st p in <.(<.q.) \/ F).) holds

ex r being Element of L st

( r in F & q "/\" r [= p )

let p, q be Element of L; :: thesis: ( p in <.(<.q.) \/ F).) implies ex r being Element of L st

( r in F & q "/\" r [= p ) )

A1: <.(<.q.) \/ F).) = { r where r is Element of L : ex p9, q9 being Element of L st

( p9 "/\" q9 [= r & p9 in <.q.) & q9 in F ) } by FILTER_0:35;

assume p in <.(<.q.) \/ F).) ; :: thesis: ex r being Element of L st

( r in F & q "/\" r [= p )

then ex r being Element of L st

( r = p & ex p9, q9 being Element of L st

( p9 "/\" q9 [= r & p9 in <.q.) & q9 in F ) ) by A1;

then consider p9, q9 being Element of L such that

A2: p9 "/\" q9 [= p and

A3: p9 in <.q.) and

A4: q9 in F ;

q [= p9 by A3, FILTER_0:15;

then q "/\" q9 [= p9 "/\" q9 by LATTICES:9;

hence ex r being Element of L st

( r in F & q "/\" r [= p ) by A2, A4, LATTICES:7; :: thesis: verum