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