let L be Lattice; :: thesis: for F being Filter of L
for p, q being Element of st p in <.(<.q.) \/ F).) holds
ex r being Element of st
( r in F & q "/\" r [= p )
let F be Filter of L; :: thesis: for p, q being Element of st p in <.(<.q.) \/ F).) holds
ex r being Element of st
( r in F & q "/\" r [= p )
let p, q be Element of ; :: thesis: ( p in <.(<.q.) \/ F).) implies ex r being Element of st
( r in F & q "/\" r [= p ) )
A1: <.(<.q.) \/ F).) = { r where r is Element of : ex p', q' being Element of st
( p' "/\" q' [= r & p' in <.q.) & q' in F ) } by FILTER_0:48;
assume p in <.(<.q.) \/ F).) ; :: thesis: ex r being Element of st
( r in F & q "/\" r [= p )
then ex r being Element of st
( r = p & ex p', q' being Element of st
( p' "/\" q' [= r & p' in <.q.) & q' in F ) ) by A1;
then consider p', q' being Element of such that
A2: p' "/\" q' [= p and
A3: p' in <.q.) and
A4: q' in F ;
q [= p' by A3, FILTER_0:18;
then q "/\" q' [= p' "/\" q' by LATTICES:27;
hence ex r being Element of st
( r in F & q "/\" r [= p ) by A2, A4, LATTICES:25; :: thesis: verum