let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra over S
for A, B being MSSubset of U0 holds
( B in SubSort A iff ( B is opers_closed & Constants U0 c= B & A c= B ) )
let U0 be MSAlgebra over S; :: thesis: for A, B being MSSubset of U0 holds
( B in SubSort A iff ( B is opers_closed & Constants U0 c= B & A c= B ) )
let A, B be MSSubset of U0; :: thesis: ( B in SubSort A iff ( B is opers_closed & Constants U0 c= B & A c= B ) )
set C = bool (Union the Sorts of U0);
A1: dom B = the carrier of S by PARTFUN1:def 2;
A2: dom the Sorts of U0 = the carrier of S by PARTFUN1:def 2;
union (rng B) c= union (rng the Sorts of U0)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng B) or x in union (rng the Sorts of U0) )
assume x in union (rng B) ; :: thesis: x in union (rng the Sorts of U0)
then consider Y being set such that
A3: x in Y and
A4: Y in rng B by TARSKI:def 4;
consider y being object such that
A5: y in dom B and
A6: B . y = Y by A4, FUNCT_1:def 3;
A7: the Sorts of U0 . y in rng the Sorts of U0 by A1, A2, A5, FUNCT_1:def 3;
B c= the Sorts of U0 by PBOOLE:def 18;
then B . y c= the Sorts of U0 . y by A1, A5;
hence x in union (rng the Sorts of U0) by A3, A6, A7, TARSKI:def 4; :: thesis: verum

end;

then bool (union (rng B)) c= bool (union (rng the Sorts of U0)) by ZFMISC_1:67;
then A8: bool (union (rng B)) c= bool (Union the Sorts of U0) by CARD_3:def 4;
thus ( B in SubSort A implies ( B is opers_closed & Constants U0 c= B & A c= B ) ) by Def10; :: thesis: ( B is opers_closed & Constants U0 c= B & A c= B implies B in SubSort A )
assume ( B is opers_closed & Constants U0 c= B & A c= B ) ; :: thesis: B in SubSort A
then A9: for C being MSSubset of U0 st C = B holds
( C is opers_closed & Constants U0 c= C & A c= C ) ;
rng B c= bool (union (rng B)) by ZFMISC_1:82;
then rng B c= bool (Union the Sorts of U0) by A8;
then B in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) by A1, FUNCT_2:def 2;
hence B in SubSort A by A9, Def10; :: thesis: verum