let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSConstants OU0 = OSCl (Constants OU0)
let OU0 be OSAlgebra of S1; :: thesis: for A being OSSubset of OU0 holds OSConstants OU0 = OSCl (Constants OU0)
let A be OSSubset of OU0; :: thesis: OSConstants OU0 = OSCl (Constants OU0)

now

let i be set ; :: thesis: ( i in the carrier of S1 implies (OSConstants OU0) . i = (OSCl (Constants OU0)) . i )
assume i in the carrier of S1 ; :: thesis: (OSConstants OU0) . i = (OSCl (Constants OU0)) . i
then reconsider s = i as SortSymbol of S1 ;
set c1 = { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } ;
set c2 = { (Constants OU0,s1) where s1 is SortSymbol of S1 : s1 <= s } ;
for x being set holds
( x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } iff x in { (Constants OU0,s1) where s1 is SortSymbol of S1 : s1 <= s } )

proof

let x be set ; :: thesis: ( x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } iff x in { (Constants OU0,s1) where s1 is SortSymbol of S1 : s1 <= s } )

hereby :: thesis: ( x in { (Constants OU0,s1) where s1 is SortSymbol of S1 : s1 <= s } implies x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } )

assume x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } ; :: thesis: x in { (Constants OU0,s1) where s1 is SortSymbol of S1 : s1 <= s }
then consider s1 being SortSymbol of S1 such that
A1: ( x = (Constants OU0) . s1 & s1 <= s ) ;
( x = Constants OU0,s1 & s1 <= s ) by A1, MSUALG_2:def 5;
hence x in { (Constants OU0,s1) where s1 is SortSymbol of S1 : s1 <= s } ; :: thesis: verum

end;

assume x in { (Constants OU0,s1) where s1 is SortSymbol of S1 : s1 <= s } ; :: thesis: x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s }
then consider s1 being SortSymbol of S1 such that
A2: ( x = Constants OU0,s1 & s1 <= s ) ;
( x = (Constants OU0) . s1 & s1 <= s ) by A2, MSUALG_2:def 5;
hence x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } ; :: thesis: verum

end;

then A3: { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } = { (Constants OU0,s1) where s1 is SortSymbol of S1 : s1 <= s } by TARSKI:2;
(OSConstants OU0) . s = OSConstants OU0,s by Def5
.= (OSCl (Constants OU0)) . s by A3, Def4 ;
hence (OSConstants OU0) . i = (OSCl (Constants OU0)) . i ; :: thesis: verum

end;

then ( ( for i being set st i in the carrier of S1 holds
(OSConstants OU0) . i c= (OSCl (Constants OU0)) . i ) & ( for i being set st i in the carrier of S1 holds
(OSCl (Constants OU0)) . i c= (OSConstants OU0) . i ) ) ;
then ( OSConstants OU0 c= OSCl (Constants OU0) & OSCl (Constants OU0) c= OSConstants OU0 ) by PBOOLE:def 5;
hence OSConstants OU0 = OSCl (Constants OU0) by PBOOLE:def 13; :: thesis: verum