let I be I_Lattice; :: thesis: for FI being Filter of I
for i, j, k being Element of I st i => j in FI holds
( i => (j "\/" k) in FI & i => (k "\/" j) in FI & (i "/\" k) => j in FI & (k "/\" i) => j in FI )
let FI be Filter of I; :: thesis: for i, j, k being Element of I st i => j in FI holds
( i => (j "\/" k) in FI & i => (k "\/" j) in FI & (i "/\" k) => j in FI & (k "/\" i) => j in FI )
let i, j, k be Element of I; :: thesis: ( i => j in FI implies ( i => (j "\/" k) in FI & i => (k "\/" j) in FI & (i "/\" k) => j in FI & (k "/\" i) => j in FI ) )
A1: i => j [= (i "/\" k) => j by Th55;
i => j [= i => (j "\/" k) by Th55;
hence ( i => j in FI implies ( i => (j "\/" k) in FI & i => (k "\/" j) in FI & (i "/\" k) => j in FI & (k "/\" i) => j in FI ) ) by A1, FILTER_0:9; :: thesis: verum