let MS be non void 1 -element segmental ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over MS
for B being non-empty MSSubAlgebra of A holds the carrier of (1-Alg B) is Subset of (1-Alg A)
let A be non-empty MSAlgebra over MS; :: thesis: for B being non-empty MSSubAlgebra of A holds the carrier of (1-Alg B) is Subset of (1-Alg A)
let B be non-empty MSSubAlgebra of A; :: thesis: the carrier of (1-Alg B) is Subset of (1-Alg A)
the Sorts of B is MSSubset of A by MSUALG_2:def 9;
then A1: the Sorts of B c= the Sorts of A by PBOOLE:def 18;
1-Alg B = UAStr(# (the_sort_of B),(the_charact_of B) #) by MSUALG_1:def 14;
then reconsider c = the carrier of (1-Alg B) as Component of the Sorts of B by MSUALG_1:def 12;
1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def 14;
then reconsider d = the carrier of (1-Alg A) as Component of the Sorts of A by MSUALG_1:def 12;
A2: dom the Sorts of A = the carrier of MS by PARTFUN1:def 2;
then consider dr being object such that
A3: dr in the carrier of MS and
A4: d = the Sorts of A . dr by FUNCT_1:def 3;
dom the Sorts of A = dom the Sorts of B by A2, PARTFUN1:def 2;
then consider cr being object such that
A5: cr in the carrier of MS and
A6: c = the Sorts of B . cr by A2, FUNCT_1:def 3;
cr = dr by A5, A3, STRUCT_0:def 10;
hence the carrier of (1-Alg B) is Subset of (1-Alg A) by A1, A5, A6, A4; :: thesis: verum