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 ;
then q "/\" q9 [= p9 "/\" q9 by LATTICES:9;
hence ex r being Element of L st
( r in F & q "/\" r [= p ) by ; :: thesis: verum