let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra over S
for A being MSSubAlgebra of U0
for o being OperSymbol of S
for x being set st x in Args (o,A) holds
x in Args (o,U0)
let U0 be MSAlgebra over S; :: thesis: for A being MSSubAlgebra of U0
for o being OperSymbol of S
for x being set st x in Args (o,A) holds
x in Args (o,U0)
let A be MSSubAlgebra of U0; :: thesis: for o being OperSymbol of S
for x being set st x in Args (o,A) holds
x in Args (o,U0)
let o be OperSymbol of S; :: thesis: for x being set st x in Args (o,A) holds
x in Args (o,U0)
let x be set ; :: thesis: ( x in Args (o,A) implies x in Args (o,U0) )
assume A1: x in Args (o,A) ; :: thesis: x in Args (o,U0)
reconsider B0 = the Sorts of A as MSSubset of U0 by MSUALG_2:def 9;
MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U0, the Charact of U0 #) ;
then U0 is MSSubAlgebra of U0 by MSUALG_2:5;
then reconsider B1 = the Sorts of U0 as MSSubset of U0 by MSUALG_2:def 9;
B0 c= B1 by PBOOLE:def 18;
then ((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o by MSUALG_2:2;
hence x in Args (o,U0) by A1; :: thesis: verum