let S be non empty non void ManySortedSign ; :: thesis:
let A be non-empty MSAlgebra over S; :: thesis:
let i be Element of S; :: thesis:
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:
let B be Equivalence_Relation of the Sorts of A; :: thesis:
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:

let ri be Element of (EqRelLatt ( the Sorts of A . i)); :: thesis:
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:

let c be Element of (EqRelLatt the Sorts of A); :: thesis:
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:
then ci in EqRelSet (X,i) by Def3;
then A6: ci [= ri by A5, LATTICE3:def 17;

let j be object ; :: thesis:
assume A7: j in the carrier of S ; :: thesis:
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;

end;

end;

end;

end;

let q9 be Element of (EqRelLatt ( the Sorts of A . i)); :: thesis:
reconsider q = q9 as Equivalence_Relation of ( the Sorts of A . i) by MSUALG_5:21;
assume q9 in EqRelSet (X,i) ; :: thesis:
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:

end;