let I be I_Lattice; 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; for i, j being Element of I holds
( i /\/ FI [= j /\/ FI iff i => j in FI )
let i, j be Element of I; ( 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 )
( i => j in FI implies i /\/ FI [= j /\/ FI )proof
assume
(i /\/ FI) "\/" (j /\/ FI) = j /\/ FI
;
LATTICES:def 3 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;
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
; 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
; LATTICES:def 3 verum