let MS be non empty trivial non void segmental ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of 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 of 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 8; :: thesis: verum