let U1, U2 be Universal_Algebra; :: thesis: ( U1 is SubAlgebra of U2 implies MSAlg U1 is MSSubAlgebra of MSAlg U2 )
assume A1: U1 is SubAlgebra of U2 ; :: thesis: MSAlg U1 is MSSubAlgebra of MSAlg U2
then MSSign U1 = MSSign U2 by Th7;
then reconsider A = MSAlg U1 as non-empty MSAlgebra over MSSign U2 ;
A is MSSubAlgebra of MSAlg U2
proof
thus the Sorts of A is MSSubset of (MSAlg U2) by A1, Th9; :: according to MSUALG_2:def 9 :: thesis: for b1 being ManySortedSubset of the Sorts of (MSAlg U2) holds
( not b1 = the Sorts of A or ( b1 is opers_closed & the Charact of A = Opers ((MSAlg U2),b1) ) )
let B be MSSubset of (MSAlg U2); :: thesis: ( not B = the Sorts of A or ( B is opers_closed & the Charact of A = Opers ((MSAlg U2),B) ) )
assume A2: B = the Sorts of A ; :: thesis: ( B is opers_closed & the Charact of A = Opers ((MSAlg U2),B) )
hence B is opers_closed by A1, Th10; :: thesis: the Charact of A = Opers ((MSAlg U2),B)
thus the Charact of A = Opers ((MSAlg U2),B) by A1, A2, Th11; :: thesis: verum
end;
hence MSAlg U1 is MSSubAlgebra of MSAlg U2 ; :: thesis: verum