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 by LATTICES:17;
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:28;
A5: i "/\" ((i "\/" j) => j) [= (i "/\" ((i "\/" j) => j)) "\/" (j "/\" ((i "\/" j) => j)) by LATTICES:22;
A6: j /\/ FI = Class (equivalence_wrt FI),j by Def6;
A7: j in Class (equivalence_wrt FI),j by EQREL_1:28;
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:30;
then (i "\/" j) <=> j in FI by FILTER_0:def 12;
then A8: (i "\/" j) => j in FI by FILTER_0:8;
A9: (i "\/" j) "/\" ((i "\/" j) => j) [= j by FILTER_0:def 8;
(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:25;
then (i "\/" j) => j [= i => j by FILTER_0:def 8;
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 by FILTER_0:2;
then A10: Top I [= j => (i "\/" j) by FILTER_0:def 8;
I is 1_Lattice ;
then Top I in FI by FILTER_0:12;
then A11: j => (i "\/" j) in FI by A10, FILTER_0:9;
A12: (i "/\" (i => j)) "\/" (j "/\" (i => j)) = (i "\/" j) "/\" (i => j) by LATTICES:def 11;
i "/\" (i => j) [= j by FILTER_0:def 8;
then (i "\/" j) "/\" (i => j) [= j by A1, A2, A12, FILTER_0:4;
then A13: i => j [= (i "\/" j) => j by FILTER_0:def 8;
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 12;
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:44
.= j /\/ FI by Def6 ; :: according to LATTICES:def 3 :: thesis: verum