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