let I be I_Lattice; :: thesis: for j, i being Element of I
for FI being Filter of I st j in FI holds
i => j in FI
let j, i 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 & i "/\" j = j "/\" i ) by LATTICES:23;
then j [= i => j by Def8;
hence ( j in FI implies i => j in FI ) by Th9; :: thesis: verum