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 1-Alg B is SubAlgebra of 1-Alg A
let A be non-empty MSAlgebra over MS; :: thesis: for B being non-empty MSSubAlgebra of A holds 1-Alg B is SubAlgebra of 1-Alg A
let B be non-empty MSSubAlgebra of A; :: thesis: 1-Alg B is SubAlgebra of 1-Alg A
( the carrier of (1-Alg B) is Subset of (1-Alg A) & ( for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
( the charact of (1-Alg B) = Opers ((1-Alg A),S) & S is opers_closed ) ) ) by Th17, Th18, Th19;
hence 1-Alg B is SubAlgebra of 1-Alg A by UNIALG_2:def 7; :: thesis: verum