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

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