let S be non empty non void ManySortedSign ; :: thesis: for A1, A2, B being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
for B1 being MSSubAlgebra of A1 st MSAlgebra(# the Sorts of B, the Charact of B #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) holds
B is MSSubAlgebra of A2
let A1, A2, B be MSAlgebra over S; :: thesis: ( MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) implies for B1 being MSSubAlgebra of A1 st MSAlgebra(# the Sorts of B, the Charact of B #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) holds
B is MSSubAlgebra of A2 )
assume A1: MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) ; :: thesis: for B1 being MSSubAlgebra of A1 st MSAlgebra(# the Sorts of B, the Charact of B #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) holds
B is MSSubAlgebra of A2
let B1 be MSSubAlgebra of A1; :: thesis: ( MSAlgebra(# the Sorts of B, the Charact of B #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) implies B is MSSubAlgebra of A2 )
assume A2: MSAlgebra(# the Sorts of B, the Charact of B #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) ; :: thesis: B is MSSubAlgebra of A2
thus the Sorts of B is MSSubset of A2 by A1, A2, MSUALG_2:def 9; :: according to MSUALG_2:def 9 :: thesis: for b₁ being ManySortedSubset of the Sorts of A2 holds
( not b₁ = the Sorts of B or ( b₁ is opers_closed & the Charact of B = Opers (A2,b₁) ) )
let C be MSSubset of A2; :: thesis: ( not C = the Sorts of B or ( C is opers_closed & the Charact of B = Opers (A2,C) ) )
reconsider C1 = C as MSSubset of A1 by A1;
assume A3: C = the Sorts of B ; :: thesis: ( C is opers_closed & the Charact of B = Opers (A2,C) )
hence C is opers_closed by A1, Th27, A2, MSUALG_2:def 9; :: thesis: the Charact of B = Opers (A2,C)
the Charact of B1 = Opers (A1,C1) by A2, A3, MSUALG_2:def 9;
hence the Charact of B = Opers (A2,C) by A1, A2, A3, MSUALG_2:def 9, Th26; :: thesis: verum