let I be I_Lattice; :: thesis: for FI being Filter of I holds I /\/ FI is implicative
let FI be Filter of I; :: thesis: I /\/ FI is implicative
set L = I /\/ FI;
set R = equivalence_wrt FI;
let x, y be Element of (I /\/ FI); :: according to FILTER_0:def 7 :: thesis: ex b₁ being Element of the carrier of (I /\/ FI) st
( x "/\" b₁ [= y & ( for b₂ being Element of the carrier of (I /\/ FI) holds
( not x "/\" b₂ [= y or b₂ [= b₁ ) ) )
A1: I is 1_Lattice by FILTER_0:37;
then A2: Top I in FI by FILTER_0:12;
A3: I /\/ FI = LattStr(# (Class (equivalence_wrt FI)),(the L_join of I /\/ (equivalence_wrt FI)),(the L_meet of I /\/ (equivalence_wrt FI)) #) by Def5;
then consider i being Element of I such that
A4: x = Class (equivalence_wrt FI),i by EQREL_1:45;
A5: x = i /\/ FI by A4, Def6;
consider j being Element of I such that
A6: y = Class (equivalence_wrt FI),j by A3, EQREL_1:45;
A7: y = j /\/ FI by A6, Def6;
take z = (i => j) /\/ FI; :: thesis: ( x "/\" z [= y & ( for b₁ being Element of the carrier of (I /\/ FI) holds
( not x "/\" b₁ [= y or b₁ [= z ) ) )
A8: i "/\" (i => j) [= j by FILTER_0:def 8;
(i "/\" (i => j)) "/\" (Top I) = i "/\" (i => j) by A1, LATTICES:43;
then Top I [= (i "/\" (i => j)) => j by A8, FILTER_0:def 8;
then (i "/\" (i => j)) => j in FI by A2, FILTER_0:9;
then (i "/\" (i => j)) /\/ FI [= y by A7, Th16;
hence x "/\" z [= y by A5, Th15; :: thesis: for b₁ being Element of the carrier of (I /\/ FI) holds
( not x "/\" b₁ [= y or b₁ [= z )
let t be Element of (I /\/ FI); :: thesis: ( not x "/\" t [= y or t [= z )
consider k being Element of I such that
A9: t = Class (equivalence_wrt FI),k by A3, EQREL_1:45;
A10: k /\/ FI = t by A9, Def6;
assume A11: x "/\" t [= y ; :: thesis: t [= z
(i /\/ FI) "/\" (k /\/ FI) = (i "/\" k) /\/ FI by Th15;
then (i "/\" k) => j in FI by A5, A7, A10, A11, Th16;
then k => (i => j) in FI by Th17;
hence t [= z by A10, Th16; :: thesis: verum