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

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