let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for s being SortSymbol of S1 holds Constants OU0,s c= OSConstants OU0,s
let OU0 be OSAlgebra of S1; :: thesis: for s being SortSymbol of S1 holds Constants OU0,s c= OSConstants OU0,s
let s be SortSymbol of S1; :: thesis: Constants OU0,s c= OSConstants OU0,s
Constants OU0,s in { (Constants OU0,s2) where s2 is SortSymbol of S1 : s2 <= s } ;
hence Constants OU0,s c= OSConstants OU0,s by ZFMISC_1:92; :: thesis: verum