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

proof

let X be set ; :: thesis: ( X in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } implies X c= the Sorts of OU0 . s )
assume X in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ; :: thesis: X c= the Sorts of OU0 . s
then consider s2 being SortSymbol of S1 such that
A1: X = Constants (OU0,s2) and
A2: s2 <= s ;
the Sorts of OU0 . s2 c= the Sorts of OU0 . s by A2, OSALG_1:def 17;
hence X c= the Sorts of OU0 . s by A1; :: thesis: verum

end;

hence union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } is Subset of ( the Sorts of OU0 . s) by ZFMISC_1:76; :: thesis: verum