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 19;
hence X c= the Sorts of OU0 . s by A1, XBOOLE_1:1; :: 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:94; :: thesis: verum