let B be B_Lattice; :: thesis: for FB being Filter of B
for I being I_Lattice
for i, j, k being Element of I
for FI being Filter of I
for a, b, c being Element of B holds
( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
let FB be Filter of B; :: thesis: for I being I_Lattice
for i, j, k being Element of I
for FI being Filter of I
for a, b, c being Element of B holds
( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
let I be I_Lattice; :: thesis: for i, j, k being Element of I
for FI being Filter of I
for a, b, c being Element of B holds
( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
let i, j, k be Element of I; :: thesis: for FI being Filter of I
for a, b, c being Element of B holds
( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
let FI be Filter of I; :: thesis: for a, b, c being Element of B holds
( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
let a, b, c be Element of B; :: thesis: ( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
thus ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) :: thesis: ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB )

proof

assume ( i <=> j in FI & j <=> k in FI ) ; :: according to FILTER_0:def 13 :: thesis: i,k are_equivalence_wrt FI
hence i <=> k in FI by Th78; :: according to FILTER_0:def 13 :: thesis: verum

end;

assume ( a <=> b in FB & b <=> c in FB ) ; :: according to FILTER_0:def 13 :: thesis: a,c are_equivalence_wrt FB
hence a <=> c in FB by Th78; :: according to FILTER_0:def 13 :: thesis: verum