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