let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over S
for i being Element of S
for X being Subset of (EqRelLatt the Sorts of A)
for B being Equivalence_Relation of the Sorts of A st B = "\/" X holds
B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i)))
let A be non-empty MSAlgebra over S; for i being Element of S
for X being Subset of (EqRelLatt the Sorts of A)
for B being Equivalence_Relation of the Sorts of A st B = "\/" X holds
B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i)))
let i be Element of S; for X being Subset of (EqRelLatt the Sorts of A)
for B being Equivalence_Relation of the Sorts of A st B = "\/" X holds
B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i)))
set M = the Sorts of A;
set E = EqRelLatt the Sorts of A;
set Ei = EqRelLatt ( the Sorts of A . i);
let X be Subset of (EqRelLatt the Sorts of A); for B being Equivalence_Relation of the Sorts of A st B = "\/" X holds
B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i)))
let B be Equivalence_Relation of the Sorts of A; ( B = "\/" X implies B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i))) )
reconsider B9 = B as Element of (EqRelLatt the Sorts of A) by MSUALG_5:def 5;
reconsider Bi = B . i as Equivalence_Relation of ( the Sorts of A . i) by MSUALG_4:def 2;
reconsider Bi9 = Bi as Element of (EqRelLatt ( the Sorts of A . i)) by MSUALG_5:21;
assume A1:
B = "\/" X
; B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i)))
then
EqRelSet (X,i) is_less_than Bi9
by LATTICE3:def 17;
hence
B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i)))
by A2, LATTICE3:def 21; verum