set L = I /\/ FI;

set R = equivalence_wrt FI;

let x, y be Element of (I /\/ FI); :: according to FILTER_0:def 6 :: thesis: ex b_{1} being Element of the carrier of (I /\/ FI) st

( x "/\" b_{1} [= y & ( for b_{2} being Element of the carrier of (I /\/ FI) holds

( not x "/\" b_{2} [= y or b_{2} [= b_{1} ) ) )

A1: Top I in FI by FILTER_0:11;

A2: 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

A3: x = Class ((equivalence_wrt FI),i) by EQREL_1:36;

A4: x = i /\/ FI by A3, Def6;

consider j being Element of I such that

A5: y = Class ((equivalence_wrt FI),j) by A2, EQREL_1:36;

A6: y = j /\/ FI by A5, Def6;

take z = (i => j) /\/ FI; :: thesis: ( x "/\" z [= y & ( for b_{1} being Element of the carrier of (I /\/ FI) holds

( not x "/\" b_{1} [= y or b_{1} [= z ) ) )

A7: i "/\" (i => j) [= j by FILTER_0:def 7;

(i "/\" (i => j)) "/\" (Top I) = i "/\" (i => j) ;

then Top I [= (i "/\" (i => j)) => j by A7, FILTER_0:def 7;

then (i "/\" (i => j)) => j in FI by A1;

then (i "/\" (i => j)) /\/ FI [= y by A6, Th16;

hence x "/\" z [= y by A4, Th15; :: thesis: for b_{1} being Element of the carrier of (I /\/ FI) holds

( not x "/\" b_{1} [= y or b_{1} [= z )

let t be Element of (I /\/ FI); :: thesis: ( not x "/\" t [= y or t [= z )

consider k being Element of I such that

A8: t = Class ((equivalence_wrt FI),k) by A2, EQREL_1:36;

A9: k /\/ FI = t by A8, Def6;

assume A10: x "/\" t [= y ; :: thesis: t [= z

(i /\/ FI) "/\" (k /\/ FI) = (i "/\" k) /\/ FI by Th15;

then (i "/\" k) => j in FI by A4, A6, A9, A10, Th16;

then k => (i => j) in FI by Th17;

hence t [= z by A9, Th16; :: thesis: verum

set R = equivalence_wrt FI;

let x, y be Element of (I /\/ FI); :: according to FILTER_0:def 6 :: thesis: ex b

( x "/\" b

( not x "/\" b

A1: Top I in FI by FILTER_0:11;

A2: 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

A3: x = Class ((equivalence_wrt FI),i) by EQREL_1:36;

A4: x = i /\/ FI by A3, Def6;

consider j being Element of I such that

A5: y = Class ((equivalence_wrt FI),j) by A2, EQREL_1:36;

A6: y = j /\/ FI by A5, Def6;

take z = (i => j) /\/ FI; :: thesis: ( x "/\" z [= y & ( for b

( not x "/\" b

A7: i "/\" (i => j) [= j by FILTER_0:def 7;

(i "/\" (i => j)) "/\" (Top I) = i "/\" (i => j) ;

then Top I [= (i "/\" (i => j)) => j by A7, FILTER_0:def 7;

then (i "/\" (i => j)) => j in FI by A1;

then (i "/\" (i => j)) /\/ FI [= y by A6, Th16;

hence x "/\" z [= y by A4, Th15; :: thesis: for b

( not x "/\" b

let t be Element of (I /\/ FI); :: thesis: ( not x "/\" t [= y or t [= z )

consider k being Element of I such that

A8: t = Class ((equivalence_wrt FI),k) by A2, EQREL_1:36;

A9: k /\/ FI = t by A8, Def6;

assume A10: x "/\" t [= y ; :: thesis: t [= z

(i /\/ FI) "/\" (k /\/ FI) = (i "/\" k) /\/ FI by Th15;

then (i "/\" k) => j in FI by A4, A6, A9, A10, Th16;

then k => (i => j) in FI by Th17;

hence t [= z by A9, Th16; :: thesis: verum