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