let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra over S
for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1

let U0 be MSAlgebra over S; :: thesis: for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1
let U1 be MSSubAlgebra of U0; :: thesis: Constants U0 is MSSubset of U1
Constants U0 c= the Sorts of U1
proof
let x be object ; :: according to PBOOLE:def 2 :: thesis: ( not x in the carrier of S or () . x c= the Sorts of U1 . x )
assume x in the carrier of S ; :: thesis: () . x c= the Sorts of U1 . x
then reconsider s = x as SortSymbol of S ;
thus (Constants U0) . x c= the Sorts of U1 . x :: thesis: verum
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in () . x or y in the Sorts of U1 . x )
per cases ( the Sorts of U0 . s = {} or the Sorts of U0 . s <> {} ) ;
suppose A1: the Sorts of U0 . s = {} ; :: thesis: ( not y in () . x or y in the Sorts of U1 . x )
() . s = Constants (U0,s) by Def4
.= {} by A1 ;
hence ( not y in () . x or y in the Sorts of U1 . x ) ; :: thesis: verum
end;
suppose the Sorts of U0 . s <> {} ; :: thesis: ( not y in () . x or y in the Sorts of U1 . x )
then A2: ex A being non empty set st
( A = the Sorts of U0 . s & Constants (U0,s) = { b where b is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & b in rng (Den (o,U0)) )
}
) by Def3;
reconsider u1 = the Sorts of U1 as MSSubset of U0 by Def9;
assume A3: y in () . x ; :: thesis: y in the Sorts of U1 . x
(Constants U0) . x = Constants (U0,s) by Def4;
then consider b being Element of the Sorts of U0 . s such that
A4: b = y and
A5: ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & b in rng (Den (o,U0)) ) by A3, A2;
consider o being OperSymbol of S such that
A6: the Arity of S . o = {} and
A7: the ResultSort of S . o = s and
A8: b in rng (Den (o,U0)) by A5;
A9: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
then A10: the Arity of S . o in rng the Arity of S by FUNCT_1:def 3;
( dom {} = {} & rng {} = {} ) ;
then reconsider a = {} as Function of {},{} by FUNCT_2:1;
A11: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
dom (u1 #) = the carrier of S * by PARTFUN1:def 2;
then o in dom ((u1 #) * the Arity of S) by ;
then A12: ((u1 #) * the Arity of S) . o = (u1 #) . ( the Arity of S . o) by FUNCT_1:12
.= (u1 #) . () by MSUALG_1:def 1
.= product (u1 * ()) by FINSEQ_2:def 5
.= product (u1 * a) by
.= by CARD_3:10 ;
dom ( the Sorts of U0 #) = the carrier of S * by PARTFUN1:def 2;
then A13: o in dom (( the Sorts of U0 #) * the Arity of S) by ;
u1 is opers_closed by Def9;
then u1 is_closed_on o ;
then A14: rng ((Den (o,U0)) | (((u1 #) * the Arity of S) . o)) c= (u1 * the ResultSort of S) . o ;
rng (Den (o,U0)) c= Result (o,U0) by RELAT_1:def 19;
then dom (Den (o,U0)) = Args (o,U0) by
.= (( the Sorts of U0 #) * the Arity of S) . o by MSUALG_1:def 4
.= ( the Sorts of U0 #) . ( the Arity of S . o) by
.= ( the Sorts of U0 #) . () by MSUALG_1:def 1
.= product ( the Sorts of U0 * ()) by FINSEQ_2:def 5
.= product ( the Sorts of U0 * a) by
.= by CARD_3:10 ;
then (Den (o,U0)) | (((u1 #) * the Arity of S) . o) = Den (o,U0) by A12;
then b in (u1 * the ResultSort of S) . o by ;
hence y in the Sorts of U1 . x by ; :: thesis: verum
end;
end;
end;
end;
hence Constants U0 is MSSubset of U1 by PBOOLE:def 18; :: thesis: verum