let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra of S holds A is MSSubAlgebra of MSAlgebra(# the Sorts of A,the Charact of A #)
let A be MSAlgebra of S; :: thesis: A is MSSubAlgebra of MSAlgebra(# the Sorts of A,the Charact of A #)
set IT = MSAlgebra(# the Sorts of A,the Charact of A #);
A1: MSAlgebra(# the Sorts of A,the Charact of A #) is MSSubAlgebra of MSAlgebra(# the Sorts of A,the Charact of A #) by MSUALG_2:6;
hence the Sorts of A is MSSubset of MSAlgebra(# the Sorts of A,the Charact of A #) by MSUALG_2:def 10; :: according to MSUALG_2:def 10 :: thesis: for b₁ being ManySortedSubset of the Sorts of MSAlgebra(# the Sorts of A,the Charact of A #) holds
( not b₁ = the Sorts of A or ( b₁ is opers_closed & the Charact of A = Opers MSAlgebra(# the Sorts of A,the Charact of A #),b₁ ) )
let C be MSSubset of MSAlgebra(# the Sorts of A,the Charact of A #); :: thesis: ( not C = the Sorts of A or ( C is opers_closed & the Charact of A = Opers MSAlgebra(# the Sorts of A,the Charact of A #),C ) )
assume A2: C = the Sorts of A ; :: thesis: ( C is opers_closed & the Charact of A = Opers MSAlgebra(# the Sorts of A,the Charact of A #),C )
hence C is opers_closed by A1, MSUALG_2:def 10; :: thesis: the Charact of A = Opers MSAlgebra(# the Sorts of A,the Charact of A #),C
thus the Charact of A = Opers MSAlgebra(# the Sorts of A,the Charact of A #),C by A1, A2, MSUALG_2:def 10; :: thesis: verum