let I be I_Lattice; :: thesis: for FI being Filter of I

for i, j, k being Element of I st i => k in FI & j => k in FI holds

(i "\/" j) => k in FI

let FI be Filter of I; :: thesis: for i, j, k being Element of I st i => k in FI & j => k in FI holds

(i "\/" j) => k in FI

let i, j, k be Element of I; :: thesis: ( i => k in FI & j => k in FI implies (i "\/" j) => k in FI )

assume that

A1: i => k in FI and

A2: j => k in FI ; :: thesis: (i "\/" j) => k in FI

A3: (i => k) "/\" (j => k) [= (i "\/" j) => k by Th56;

(i => k) "/\" (j => k) in FI by A1, A2, FILTER_0:8;

hence (i "\/" j) => k in FI by A3, FILTER_0:9; :: thesis: verum

for i, j, k being Element of I st i => k in FI & j => k in FI holds

(i "\/" j) => k in FI

let FI be Filter of I; :: thesis: for i, j, k being Element of I st i => k in FI & j => k in FI holds

(i "\/" j) => k in FI

let i, j, k be Element of I; :: thesis: ( i => k in FI & j => k in FI implies (i "\/" j) => k in FI )

assume that

A1: i => k in FI and

A2: j => k in FI ; :: thesis: (i "\/" j) => k in FI

A3: (i => k) "/\" (j => k) [= (i "\/" j) => k by Th56;

(i => k) "/\" (j => k) in FI by A1, A2, FILTER_0:8;

hence (i "\/" j) => k in FI by A3, FILTER_0:9; :: thesis: verum