let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra over S

for A being MSSubset of U0 holds the Sorts of U0 in SubSort A

let U0 be MSAlgebra over S; :: thesis: for A being MSSubset of U0 holds the Sorts of U0 in SubSort A

let A be MSSubset of U0; :: thesis: the Sorts of U0 in SubSort A

set f = Funcs ( the carrier of S,(bool (Union the Sorts of U0)));

Union the Sorts of U0 = union (rng the Sorts of U0) by CARD_3:def 4;

then ( dom the Sorts of U0 = the carrier of S & rng the Sorts of U0 c= bool (Union the Sorts of U0) ) by PARTFUN1:def 2, ZFMISC_1:82;

then A1: the Sorts of U0 in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) by FUNCT_2:def 2;

( the Sorts of U0 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of U0 holds

( B is opers_closed & Constants U0 c= B & A c= B ) ) ) by Th3, PBOOLE:def 18;

hence the Sorts of U0 in SubSort A by A1, Def10; :: thesis: verum

for A being MSSubset of U0 holds the Sorts of U0 in SubSort A

let U0 be MSAlgebra over S; :: thesis: for A being MSSubset of U0 holds the Sorts of U0 in SubSort A

let A be MSSubset of U0; :: thesis: the Sorts of U0 in SubSort A

set f = Funcs ( the carrier of S,(bool (Union the Sorts of U0)));

Union the Sorts of U0 = union (rng the Sorts of U0) by CARD_3:def 4;

then ( dom the Sorts of U0 = the carrier of S & rng the Sorts of U0 c= bool (Union the Sorts of U0) ) by PARTFUN1:def 2, ZFMISC_1:82;

then A1: the Sorts of U0 in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) by FUNCT_2:def 2;

( the Sorts of U0 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of U0 holds

( B is opers_closed & Constants U0 c= B & A c= B ) ) ) by Th3, PBOOLE:def 18;

hence the Sorts of U0 in SubSort A by A1, Def10; :: thesis: verum