let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1 holds Constants OU0 c= OSConstants OU0
let OU0 be OSAlgebra of S1; :: thesis: Constants OU0 c= OSConstants OU0
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in the carrier of S1 or (Constants OU0) . i c= (OSConstants OU0) . i )
assume i in the carrier of S1 ; :: thesis: (Constants OU0) . i c= (OSConstants OU0) . i
then reconsider s = i as SortSymbol of S1 ;
( (Constants OU0) . s = Constants (OU0,s) & (OSConstants OU0) . s = OSConstants (OU0,s) ) by Def5, MSUALG_2:def 4;
hence (Constants OU0) . i c= (OSConstants OU0) . i by Th6; :: thesis: verum