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:74; :: thesis: verum