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 ) )
assume A1: p in <.(<.q.) \/ F).) ; :: thesis: ex r being Element of L st
( r in F & q "/\" r [= p )
<.(<.q.) \/ F).) = { r where r is Element of L : ex p', q' being Element of L st
( p' "/\" q' [= r & p' in <.q.) & q' in F ) } by FILTER_0:48;
then ex r being Element of L st
( r = p & ex p', q' being Element of L st
( p' "/\" q' [= r & p' in <.q.) & q' in F ) ) by A1;
then consider p', q' being Element of L such that
A2: ( p' "/\" q' [= p & p' in <.q.) & q' in F ) ;
q [= p' by A2, FILTER_0:18;
then q "/\" q' [= p' "/\" q' by LATTICES:27;
hence ex r being Element of L st
( r in F & q "/\" r [= p ) by A2, LATTICES:25; :: thesis: verum