let I be I_Lattice; :: thesis: for FI being Filter of I
for i, k, j being Element of I st i => k in FI & j => k in FI holds
(i "\/" j) => k in FI
let FI be Filter of I; :: thesis: for i, k, j being Element of I st i => k in FI & j => k in FI holds
(i "\/" j) => k in FI
let i, k, j be Element of I; :: thesis: ( i => k in FI & j => k in FI implies (i "\/" j) => k in FI )
A1: (i => k) "/\" (j => k) [= (i "\/" j) => k by Th57;
assume ( i => k in FI & j => k in FI ) ; :: thesis: (i "\/" j) => k in FI
then (i => k) "/\" (j => k) in FI by FILTER_0:def 1;
hence (i "\/" j) => k in FI by A1, FILTER_0:9; :: thesis: verum