let I be I_Lattice; :: thesis: for i, j being Element of I
for FI being Filter of I st i in FI & i => j in FI holds
j in FI
let i, j be Element of I; :: thesis: for FI being Filter of I st i in FI & i => j in FI holds
j in FI
let FI be Filter of I; :: thesis: ( i in FI & i => j in FI implies j in FI )
assume ( i in FI & i => j in FI ) ; :: thesis: j in FI
then A1: i "/\" (i => j) in FI by Th8;
i "/\" (i => j) [= j by Def7;
hence j in FI by A1, Th9; :: thesis: verum