let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for OU1 being OSSubAlgebra of OU0 holds OSConstants OU0 is OSSubset of OU1
let OU0 be OSAlgebra of S1; :: thesis: for OU1 being OSSubAlgebra of OU0 holds OSConstants OU0 is OSSubset of OU1
let OU1 be OSSubAlgebra of OU0; :: thesis: OSConstants OU0 is OSSubset of OU1
OSConstants OU0 c= the Sorts of OU1

proof

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in the carrier of S1 or (OSConstants OU0) . i c= the Sorts of OU1 . i )
assume i in the carrier of S1 ; :: thesis: (OSConstants OU0) . i c= the Sorts of OU1 . i
then reconsider s = i as SortSymbol of S1 ;
Constants OU0 is MSSubset of OU1 by MSUALG_2:10;
then A1: Constants OU0 c= the Sorts of OU1 by PBOOLE:def 18;
A2: for s2, s3 being SortSymbol of S1 st s2 <= s3 holds
(Constants OU0) . s2 c= the Sorts of OU1 . s3

proof

let s2, s3 be SortSymbol of S1; :: thesis: ( s2 <= s3 implies (Constants OU0) . s2 c= the Sorts of OU1 . s3 )
assume s2 <= s3 ; :: thesis: (Constants OU0) . s2 c= the Sorts of OU1 . s3
then A3: the Sorts of OU1 . s2 c= the Sorts of OU1 . s3 by OSALG_1:def 17;
(Constants OU0) . s2 c= the Sorts of OU1 . s2 by A1;
hence (Constants OU0) . s2 c= the Sorts of OU1 . s3 by A3; :: thesis: verum

end;

A4: for X being set st X in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } holds
X c= the Sorts of OU1 . s

proof

let X be set ; :: thesis: ( X in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } implies X c= the Sorts of OU1 . s )
assume X in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } ; :: thesis: X c= the Sorts of OU1 . s
then consider s4 being SortSymbol of S1 such that
A5: ( X = Constants (OU0,s4) & s4 <= s ) ;
Constants (OU0,s4) = (Constants OU0) . s4 by MSUALG_2:def 4;
hence X c= the Sorts of OU1 . s by A2, A5; :: thesis: verum

end;

(OSConstants OU0) . i = OSConstants (OU0,s) by Def5
.= union { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } ;
hence (OSConstants OU0) . i c= the Sorts of OU1 . i by A4, ZFMISC_1:76; :: thesis: verum

end;

then A6: OSConstants OU0 is ManySortedSubset of the Sorts of OU1 by PBOOLE:def 18;
OSConstants OU0 is OrderSortedSet of S1 by Def2;
hence OSConstants OU0 is OSSubset of OU1 by A6, Def2; :: thesis: verum