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