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 that
A1: i => j in FI and
A2: j => k in FI ; :: thesis: i => k in FI
A3: FI \/ {i} c= <.(FI \/ {i}).) by Def4;
{i} c= FI \/ {i} by XBOOLE_1:7;
then A4: {i} c= <.(FI \/ {i}).) by A3;
FI c= FI \/ {i} by XBOOLE_1:7;
then A5: FI c= <.(FI \/ {i}).) by A3;
i in {i} by TARSKI:def 1;
then j in <.(FI \/ {i}).) by A1, A5, A4, Th29;
then A6: k in <.(FI \/ {i}).) by A2, A5, Th29;
<.FI.) = FI by Th21;
hence i => k in FI by A6, Th40; :: thesis: verum