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 set ; :: according to PBOOLE:def 5 :: 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:11;
then A1: Constants OU0 c= the Sorts of OU1 by PBOOLE:def 23;
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 19;
(Constants OU0) . s2 c= the Sorts of OU1 . s2 by A1, PBOOLE:def 5;
hence (Constants OU0) . s2 c= the Sorts of OU1 . s3 by A3, XBOOLE_1:1; :: 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 5;
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:94; :: thesis: verum

end;

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