let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U0 being MSAlgebra over S
for A, B being MSSubset of U0 st B in SubSort A holds
((() #) * the Arity of S) . o c= ((B #) * the Arity of S) . o

let o be OperSymbol of S; :: thesis: for U0 being MSAlgebra over S
for A, B being MSSubset of U0 st B in SubSort A holds
((() #) * the Arity of S) . o c= ((B #) * the Arity of S) . o

let U0 be MSAlgebra over S; :: thesis: for A, B being MSSubset of U0 st B in SubSort A holds
((() #) * the Arity of S) . o c= ((B #) * the Arity of S) . o

let A, B be MSSubset of U0; :: thesis: ( B in SubSort A implies ((() #) * the Arity of S) . o c= ((B #) * the Arity of S) . o )
assume A1: B in SubSort A ; :: thesis: ((() #) * the Arity of S) . o c= ((B #) * the Arity of S) . o
MSSubSort A c= B
proof
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in the carrier of S or () . i c= B . i )
assume i in the carrier of S ; :: thesis: () . i c= B . i
then reconsider s = i as SortSymbol of S ;
( (MSSubSort A) . s = meet (SubSort (A,s)) & B . s in SubSort (A,s) ) by ;
hence (MSSubSort A) . i c= B . i by SETFAM_1:3; :: thesis: verum
end;
hence (((MSSubSort A) #) * the Arity of S) . o c= ((B #) * the Arity of S) . o by Th2; :: thesis: verum