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