let I be I_Lattice; :: thesis: for FI being Filter of I
for i, j being Element of I holds
( i /\/ FI [= j /\/ FI iff i => j in FI )
let FI be Filter of I; :: thesis: for i, j being Element of I holds
( i /\/ FI [= j /\/ FI iff i => j in FI )
let i, j be Element of I; :: thesis: ( i /\/ FI [= j /\/ FI iff i => j in FI )
set R = equivalence_wrt FI;
set a = i "\/" j;
set b = (i "\/" j) => j;
A1: j "/\" (i => j) [= j by FILTER_0:2;
A2: j "\/" j = j ;
thus ( i /\/ FI [= j /\/ FI implies i => j in FI ) :: thesis: ( i => j in FI implies i /\/ FI [= j /\/ FI )
proof
assume (i /\/ FI) "\/" (j /\/ FI) = j /\/ FI ; :: according to LATTICES:def 3 :: thesis: i => j in FI
then A3: (i "\/" j) /\/ FI = j /\/ FI by Th15;
A4: i "\/" j in Class ((equivalence_wrt FI),(i "\/" j)) by EQREL_1:20;
A5: i "/\" ((i "\/" j) => j) [= (i "/\" ((i "\/" j) => j)) "\/" (j "/\" ((i "\/" j) => j)) by LATTICES:5;
A6: j /\/ FI = Class ((equivalence_wrt FI),j) by Def6;
A7: j in Class ((equivalence_wrt FI),j) by EQREL_1:20;
Class ((equivalence_wrt FI),(i "\/" j)) = (i "\/" j) /\/ FI by Def6;
then [(i "\/" j),j] in equivalence_wrt FI by A3, A6, A4, A7, EQREL_1:22;
then (i "\/" j) <=> j in FI by FILTER_0:def 11;
then A8: (i "\/" j) => j in FI by FILTER_0:8;
A9: (i "\/" j) "/\" ((i "\/" j) => j) [= j by FILTER_0:def 7;
(i "\/" j) "/\" ((i "\/" j) => j) = (i "/\" ((i "\/" j) => j)) "\/" (j "/\" ((i "\/" j) => j)) by LATTICES:def 11;
then i "/\" ((i "\/" j) => j) [= j by A9, A5, LATTICES:7;
then (i "\/" j) => j [= i => j by FILTER_0:def 7;
hence i => j in FI by A8, FILTER_0:9; :: thesis: verum
end;
j [= i "\/" j by FILTER_0:3;
then j "/\" (Top I) [= i "\/" j ;
then A10: Top I [= j => (i "\/" j) by FILTER_0:def 7;
Top I in FI by FILTER_0:11;
then A11: j => (i "\/" j) in FI by A10;
A12: (i "/\" (i => j)) "\/" (j "/\" (i => j)) = (i "\/" j) "/\" (i => j) by LATTICES:def 11;
i "/\" (i => j) [= j by FILTER_0:def 7;
then (i "\/" j) "/\" (i => j) [= j by A1, A2, A12, FILTER_0:4;
then A13: i => j [= (i "\/" j) => j by FILTER_0:def 7;
assume i => j in FI ; :: thesis: i /\/ FI [= j /\/ FI
then (i "\/" j) => j in FI by A13, FILTER_0:9;
then (i "\/" j) <=> j in FI by A11, FILTER_0:8;
then A14: [(i "\/" j),j] in equivalence_wrt FI by FILTER_0:def 11;
thus (i /\/ FI) "\/" (j /\/ FI) = (i "\/" j) /\/ FI by Th15
.= Class ((equivalence_wrt FI),(i "\/" j)) by Def6
.= Class ((equivalence_wrt FI),j) by A14, EQREL_1:35
.= j /\/ FI by Def6 ; :: according to LATTICES:def 3 :: thesis: verum