let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ; :: thesis: B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i)))

A2: now :: thesis: for ri being Element of (EqRelLatt ( the Sorts of A . i)) st EqRelSet (X,i) is_less_than ri holds
Bi9 [= ri

let ri be Element of (EqRelLatt ( the Sorts of A . i)); :: thesis: ( EqRelSet (X,i) is_less_than ri implies Bi9 [= ri )
reconsider ri9 = ri as Equivalence_Relation of ( the Sorts of A . i) by MSUALG_5:21;
consider r9 being Equivalence_Relation of the Sorts of A such that
A3: r9 . i = ri9 and
A4: for j being SortSymbol of S st j <> i holds
r9 . j = nabla ( the Sorts of A . j) by Th16;
reconsider r = r9 as Element of (EqRelLatt the Sorts of A) by MSUALG_5:def 5;
assume A5: EqRelSet (X,i) is_less_than ri ; :: thesis: Bi9 [= ri

now :: thesis: for c being Element of (EqRelLatt the Sorts of A) st c in X holds
c [= r

let c be Element of (EqRelLatt the Sorts of A); :: thesis: ( c in X implies c [= r )
reconsider c9 = c as Equivalence_Relation of the Sorts of A by MSUALG_5:def 5;
reconsider ci9 = c9 . i as Equivalence_Relation of ( the Sorts of A . i) by MSUALG_4:def 2;
reconsider ci = ci9 as Element of (EqRelLatt ( the Sorts of A . i)) by MSUALG_5:21;
assume c in X ; :: thesis: c [= r
then ci in EqRelSet (X,i) by Def3;
then A6: ci [= ri by A5, LATTICE3:def 17;

now :: thesis: for j being object st j in the carrier of S holds
c9 . j c= r9 . j

let j be object ; :: thesis: ( j in the carrier of S implies c9 . b₁ c= r9 . b₁ )
assume A7: j in the carrier of S ; :: thesis: c9 . b₁ c= r9 . b₁
then reconsider j9 = j as Element of S ;
reconsider rj9 = r9 . j9, cj9 = c9 . j9 as Equivalence_Relation of ( the Sorts of A . j) by MSUALG_4:def 2;

per cases ( j = i or j <> i ) ;

suppose j = i ; :: thesis: c9 . b₁ c= r9 . b₁

hence c9 . j c= r9 . j by A3, A6, Th2; :: thesis: verum

end;

suppose j <> i ; :: thesis: c9 . b₁ c= r9 . b₁

then r9 . j = nabla ( the Sorts of A . j) by A4, A7;
then cj9 /\ rj9 = cj9 by XBOOLE_1:28;
hence c9 . j c= r9 . j by XBOOLE_1:17; :: thesis: verum

end;

end;

end;

then c9 c= r9 by PBOOLE:def 2;
hence c [= r by MSUALG_7:6; :: thesis: verum

end;

then X is_less_than r by LATTICE3:def 17;
then B9 [= r by A1, LATTICE3:def 21;
then B c= r9 by MSUALG_7:6;
then Bi c= ri9 by A3, PBOOLE:def 2;
hence Bi9 [= ri by Th2; :: thesis: verum

end;

now :: thesis: for q9 being Element of (EqRelLatt ( the Sorts of A . i)) st q9 in EqRelSet (X,i) holds
q9 [= Bi9

let q9 be Element of (EqRelLatt ( the Sorts of A . i)); :: thesis: ( q9 in EqRelSet (X,i) implies q9 [= Bi9 )
reconsider q = q9 as Equivalence_Relation of ( the Sorts of A . i) by MSUALG_5:21;
assume q9 in EqRelSet (X,i) ; :: thesis: q9 [= Bi9
then consider Eq being Equivalence_Relation of the Sorts of A such that
A8: q9 = Eq . i and
A9: Eq in X by Def3;
reconsider Eq9 = Eq as Element of (EqRelLatt the Sorts of A) by MSUALG_5:def 5;
Eq9 [= B9 by A1, A9, LATTICE3:38;
then Eq c= B by MSUALG_7:6;
then q c= Bi by A8, PBOOLE:def 2;
hence q9 [= Bi9 by Th2; :: thesis: verum

end;

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; :: thesis: verum