let I be I_Lattice; :: thesis: for FI being Filter of I
for i, j, k 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, j, k 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, j, k 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 ;
then A5: (i "/\" j) <=> k in FI by A3, A4, Th58;
k "\/" k = k ;
then (i "\/" j) <=> k in FI by A3, A4, Th58;
hence ( i "\/" j in Class ((equivalence_wrt FI),k) & i "/\" j in Class ((equivalence_wrt FI),k) ) by A5, Lm4; :: thesis: verum