reconsider I = L as I_Lattice by A1;

let c1, c2 be Element of (L /\/ F); :: thesis: ( ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

c1 = Class (R,a) ) & ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

c2 = Class (R,a) ) implies c1 = c2 )

assume that

A2: for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

c1 = Class (R,a) and

A3: for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

c2 = Class (R,a) ; :: thesis: c1 = c2

reconsider FI = F as Filter of I ;

c1 = Class ((equivalence_wrt FI),a) by A2;

hence c1 = c2 by A3; :: thesis: verum

let c1, c2 be Element of (L /\/ F); :: thesis: ( ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

c1 = Class (R,a) ) & ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

c2 = Class (R,a) ) implies c1 = c2 )

assume that

A2: for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

c1 = Class (R,a) and

A3: for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

c2 = Class (R,a) ; :: thesis: c1 = c2

reconsider FI = F as Filter of I ;

c1 = Class ((equivalence_wrt FI),a) by A2;

hence c1 = c2 by A3; :: thesis: verum