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 )

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

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

j [= i "\/" j
by FILTER_0:3;
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;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

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