let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra over S
for B being MSSubAlgebra of A
for s being SortSymbol of S
for a being set st a in the Sorts of B . s holds
a in the Sorts of A . s
let A be MSAlgebra over S; :: thesis: for B being MSSubAlgebra of A
for s being SortSymbol of S
for a being set st a in the Sorts of B . s holds
a in the Sorts of A . s
let B be MSSubAlgebra of A; :: thesis: for s being SortSymbol of S
for a being set st a in the Sorts of B . s holds
a in the Sorts of A . s
let s be SortSymbol of S; :: thesis: for a being set st a in the Sorts of B . s holds
a in the Sorts of A . s
the Sorts of B is MSSubset of A by MSUALG_2:def 9;
then the Sorts of B . s c= the Sorts of A . s by PBOOLE:def 18, PBOOLE:def 2;
hence for a being set st a in the Sorts of B . s holds
a in the Sorts of A . s ; :: thesis: verum