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