let I be I_Lattice; :: thesis: for FI being Filter of I
for i, k, j being Element of I st i in Class ((equivalence_wrt FI),k) & j in Class ((equivalence_wrt FI),k) holds
( i "\/" j in Class ((equivalence_wrt FI),k) & i "/\" j in Class ((equivalence_wrt FI),k) )
let FI be Filter of I; :: thesis: for i, k, j being Element of I st i in Class ((equivalence_wrt FI),k) & j in Class ((equivalence_wrt FI),k) holds
( i "\/" j in Class ((equivalence_wrt FI),k) & i "/\" j in Class ((equivalence_wrt FI),k) )
let i, k, j be Element of I; :: thesis: ( i in Class ((equivalence_wrt FI),k) & j in Class ((equivalence_wrt FI),k) implies ( i "\/" j in Class ((equivalence_wrt FI),k) & i "/\" j in Class ((equivalence_wrt FI),k) ) )
assume that
A1: i in Class ((equivalence_wrt FI),k) and
A2: j in Class ((equivalence_wrt FI),k) ; :: thesis: ( i "\/" j in Class ((equivalence_wrt FI),k) & i "/\" j in Class ((equivalence_wrt FI),k) )
A3: i <=> k in FI by A1, Lm4;
A4: j <=> k in FI by A2, Lm4;
k "/\" k = k by LATTICES:18;
then A5: (i "/\" j) <=> k in FI by A3, A4, Th59;
k "\/" k = k by LATTICES:17;
then (i "\/" j) <=> k in FI by A3, A4, Th59;
hence ( i "\/" j in Class ((equivalence_wrt FI),k) & i "/\" j in Class ((equivalence_wrt FI),k) ) by A5, Lm4; :: thesis: verum