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 ( i in Class (equivalence_wrt FI),k & j in Class (equivalence_wrt FI),k ) ; :: thesis: ( i "\/" j in Class (equivalence_wrt FI),k & i "/\" j in Class (equivalence_wrt FI),k )
then ( i <=> k in FI & j <=> k in FI & k "\/" k = k & k "/\" k = k ) by Lm4, LATTICES:17, LATTICES:18;
then ( (i "\/" j) <=> k in FI & (i "/\" j) <=> k in FI ) by Th59;
hence ( i "\/" j in Class (equivalence_wrt FI),k & i "/\" j in Class (equivalence_wrt FI),k ) by Lm4; :: thesis: verum