let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of 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 of 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 3;
reconsider Bi9 = Bi as Element of (EqRelLatt (the Sorts of A . i)) by MSUALG_5:23;
assume A1: B = "\/" X ; :: thesis: B . i = "\/" (EqRelSet X,i),(EqRelLatt (the Sorts of A . i))

A2: now

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:23;
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

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 3;
reconsider ci = ci9 as Element of (EqRelLatt (the Sorts of A . i)) by MSUALG_5:23;
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

let j be set ; :: 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 3;

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 5;
hence c [= r by MSUALG_7:7; :: 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:7;
then Bi c= ri9 by A3, PBOOLE:def 5;
hence Bi9 [= ri by Th2; :: thesis: verum

end;

now

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:23;
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:7;
then q c= Bi by A8, PBOOLE:def 5;
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