let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for R being ManySortedRelation of the Sorts of A
for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in (StabCl R) . s iff ex x, y being Element of A,s ex h being Endomorphism of A st
( [x,y] in R . s & a = (h . s) . x & b = (h . s) . y ) )
let A be non-empty MSAlgebra of S; :: thesis: for R being ManySortedRelation of the Sorts of A
for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in (StabCl R) . s iff ex x, y being Element of A,s ex h being Endomorphism of A st
( [x,y] in R . s & a = (h . s) . x & b = (h . s) . y ) )
let P be ManySortedRelation of the Sorts of A; :: thesis: for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in (StabCl P) . s iff ex x, y being Element of A,s ex h being Endomorphism of A st
( [x,y] in P . s & a = (h . s) . x & b = (h . s) . y ) )
defpred S₁[ SortSymbol of S, set , set ] means ex s' being SortSymbol of S ex f being Function of the Sorts of A . s',the Sorts of A . $1 ex x, y being Element of A,s' st
( s' = $1 & ex h being Endomorphism of A st f = h . s' & [x,y] in P . s' & $2 = f . x & $3 = f . y );
consider Q being ManySortedRelation of the Sorts of A such that
A1: for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff S₁[s,a,b] ) from MSUALG_6:sch 2();
reconsider R = P, Q = Q as ManySortedRelation of A ;
A2: ( Q is stable & R c= Q & ( for P being ManySortedRelation of A st P is stable & R c= P holds
Q c= P ) ) by A1, Lm2;
reconsider Q = Q as stable ManySortedRelation of A by A1, Lm2;
A3: StabCl R = Q

proof

R c= StabCl R by Def12;
hence ( StabCl R c= Q & Q c= StabCl R ) by A2, Def12; :: according to PBOOLE:def 13 :: thesis: verum

end;

let s be SortSymbol of S; :: thesis: for a, b being Element of A,s holds
( [a,b] in (StabCl P) . s iff ex x, y being Element of A,s ex h being Endomorphism of A st
( [x,y] in P . s & a = (h . s) . x & b = (h . s) . y ) )
let a, b be Element of A,s; :: thesis: ( [a,b] in (StabCl P) . s iff ex x, y being Element of A,s ex h being Endomorphism of A st
( [x,y] in P . s & a = (h . s) . x & b = (h . s) . y ) )

hereby :: thesis: ( ex x, y being Element of A,s ex h being Endomorphism of A st
( [x,y] in P . s & a = (h . s) . x & b = (h . s) . y ) implies [a,b] in (StabCl P) . s )

assume [a,b] in (StabCl P) . s ; :: thesis: ex x, y being Element of A,s ex h being Endomorphism of A st
( [x,y] in P . s & a = (h . s) . x & b = (h . s) . y )
then ex s' being SortSymbol of S ex f being Function of the Sorts of A . s',the Sorts of A . s ex x, y being Element of A,s' st
( s' = s & ex h being Endomorphism of A st f = h . s' & [x,y] in P . s' & a = f . x & b = f . y ) by A1, A3;
hence ex x, y being Element of A,s ex h being Endomorphism of A st
( [x,y] in P . s & a = (h . s) . x & b = (h . s) . y ) ; :: thesis: verum

end;

thus ( ex x, y being Element of A,s ex h being Endomorphism of A st
( [x,y] in P . s & a = (h . s) . x & b = (h . s) . y ) implies [a,b] in (StabCl P) . s ) by A1, A3; :: thesis: verum