let L be Lattice; :: thesis: for F being Filter of L st L is I_Lattice holds
latt F is implicative
let F be Filter of L; :: thesis: ( L is I_Lattice implies latt F is implicative )
assume A1: L is I_Lattice ; :: thesis: latt F is implicative
then reconsider I = L as I_Lattice ;
reconsider FI = F as Filter of I ;
let p9, q9 be Element of (latt F); :: according to FILTER_0:def 6 :: thesis: ex r being Element of (latt F) st
( p9 "/\" r [= q9 & ( for r1 being Element of (latt F) st p9 "/\" r1 [= q9 holds
r1 [= r ) )
reconsider p = p9, q = q9 as Element of F by Th49;
consider r being Element of L such that
A2: p "/\" r [= q and
A3: for r1 being Element of L st p "/\" r1 [= q holds
r1 [= r by A1, Def6;
reconsider i = p, j = q as Element of I ;
A4: i => j in FI by Th30;
i => j = r by A2, A3, Def7;
then reconsider r9 = r as Element of (latt F) by A4, Th49;
take r9 ; :: thesis: ( p9 "/\" r9 [= q9 & ( for r1 being Element of (latt F) st p9 "/\" r1 [= q9 holds
r1 [= r9 ) )
p "/\" r = p9 "/\" r9 by Th50;
hence p9 "/\" r9 [= q9 by A2, Th51; :: thesis: for r1 being Element of (latt F) st p9 "/\" r1 [= q9 holds
r1 [= r9
let s9 be Element of (latt F); :: thesis: ( p9 "/\" s9 [= q9 implies s9 [= r9 )
assume A5: p9 "/\" s9 [= q9 ; :: thesis: s9 [= r9
reconsider s = s9 as Element of F by Th49;
p "/\" s = p9 "/\" s9 by Th50;
then p "/\" s [= q by A5, Th51;
then s [= r by A3;
hence s9 [= r9 by Th51; :: thesis: verum