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

A2: now

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

now

let c be Element of ; :: thesis: ( c in X implies c [= r )
reconsider c' = c as Equivalence_Relation of the Sorts of A by MSUALG_5:def 5;
reconsider ci' = c' . i as Equivalence_Relation of by MSUALG_4:def 3;
reconsider ci = ci' as Element of by MSUALG_7:1;
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 c' . b₁ c= r' . b₁ )
assume A7: j in the carrier of S ; :: thesis: c' . b₁ c= r' . b₁
then reconsider j' = j as Element of ;
reconsider rj' = r' . j', cj' = c' . j' as Equivalence_Relation of by MSUALG_4:def 3;

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

suppose j = i ; :: thesis: c' . b₁ c= r' . b₁

hence c' . j c= r' . j by A3, A6, Th2; :: thesis: verum

end;

suppose j <> i ; :: thesis: c' . b₁ c= r' . b₁

then r' . j = nabla (the Sorts of A . j) by A4, A7;
then cj' /\ rj' = cj' by XBOOLE_1:28;
hence c' . j c= r' . j by XBOOLE_1:17; :: thesis: verum

end;

end;

end;

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

end;

now

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

end;

then EqRelSet X,i is_less_than Bi' by LATTICE3:def 17;
hence B . i = "\/" (EqRelSet X,i),(EqRelLatt (the Sorts of A . i)) by A2, LATTICE3:def 21; :: thesis: verum