let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra over S
for A being MSSubset of U0 holds
( MSSubSort A is opers_closed & A c= MSSubSort A )
let U0 be MSAlgebra over S; :: thesis: for A being MSSubset of U0 holds
( MSSubSort A is opers_closed & A c= MSSubSort A )
let A be MSSubset of U0; :: thesis: ( MSSubSort A is opers_closed & A c= MSSubSort A )
thus MSSubSort A is opers_closed :: thesis: A c= MSSubSort A

proof

let o be OperSymbol of S; :: according to MSUALG_2:def 6 :: thesis: MSSubSort A is_closed_on o
rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o by Th19;
hence MSSubSort A is_closed_on o ; :: thesis: verum

end;

( A c= (Constants U0) (\/) A & (Constants U0) (\/) A c= MSSubSort A ) by Th15, PBOOLE:14;
hence A c= MSSubSort A by PBOOLE:13; :: thesis: verum