let I be I_Lattice; :: thesis: for i, j, k being Element of I
for FI being Filter of I st i <=> j in FI & j <=> k in FI holds
i <=> k in FI
let i, j, k be Element of I; :: thesis: for FI being Filter of I st i <=> j in FI & j <=> k in FI holds
i <=> k in FI
let FI be Filter of I; :: thesis: ( i <=> j in FI & j <=> k in FI implies i <=> k in FI )
assume A1: ( i <=> j in FI & j <=> k in FI ) ; :: thesis: i <=> k in FI
then ( j => i in FI & k => j in FI ) by Th8;
then A2: k => i in FI by Th41;
( i => j in FI & j => k in FI ) by A1, Th8;
then i => k in FI by Th41;
hence i <=> k in FI by A2, Th8; :: thesis: verum