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 b1 being Element of the carrier of (I /\/ FI) st
( x "/\" b1 [= y & ( for b2 being Element of the carrier of (I /\/ FI) holds
( not x "/\" b2 [= y or b2 [= b1 ) ) )

A1: Top I in FI by FILTER_0:11;
A2: I /\/ FI = LattStr(# (Class ()),( the L_join of I /\/ ()),( the L_meet of I /\/ ()) #) by Def5;
then consider i being Element of I such that
A3: x = Class ((),i) by EQREL_1:36;
A4: x = i /\/ FI by ;
consider j being Element of I such that
A5: y = Class ((),j) by ;
A6: y = j /\/ FI by ;
take z = (i => j) /\/ FI; :: thesis: ( x "/\" z [= y & ( for b1 being Element of the carrier of (I /\/ FI) holds
( not x "/\" b1 [= y or b1 [= 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 ;
then (i "/\" (i => j)) => j in FI by A1;
then (i "/\" (i => j)) /\/ FI [= y by ;
hence x "/\" z [= y by ; :: thesis: for b1 being Element of the carrier of (I /\/ FI) holds
( not x "/\" b1 [= y or b1 [= 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 ((),k) by ;
A9: k /\/ FI = t by ;
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 ; :: thesis: verum