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
let p', q' be Element of (latt F); :: according to FILTER_0:def 7 :: thesis: ex r being Element of (latt F) st
( p' "/\" r [= q' & ( for r1 being Element of (latt F) st p' "/\" r1 [= q' holds
r1 [= r ) )
reconsider p = p', q = q' as Element of F by Th63;
consider r being Element of L such that
A2: ( p "/\" r [= q & ( for r1 being Element of L st p "/\" r1 [= q holds
r1 [= r ) ) by A1, Def7;
reconsider I = L as I_Lattice by A1;
reconsider i = p, j = q as Element of I ;
reconsider FI = F as Filter of I ;
( i => j = r & i => j in FI ) by A2, Def8, Th42;
then reconsider r' = r as Element of (latt F) by Th63;
take r' ; :: thesis: ( p' "/\" r' [= q' & ( for r1 being Element of (latt F) st p' "/\" r1 [= q' holds
r1 [= r' ) )
p "/\" r = p' "/\" r' by Th64;
hence p' "/\" r' [= q' by A2, Th65; :: thesis: for r1 being Element of (latt F) st p' "/\" r1 [= q' holds
r1 [= r'
let s' be Element of (latt F); :: thesis: ( p' "/\" s' [= q' implies s' [= r' )
assume A3: p' "/\" s' [= q' ; :: thesis: s' [= r'
reconsider s = s' as Element of F by Th63;
p "/\" s = p' "/\" s' by Th64;
then p "/\" s [= q by A3, Th65;
then s [= r by A2;
hence s' [= r' by Th65; :: thesis: verum