let U1, U2 be Universal_Algebra; :: thesis: ( MSAlg U1 is MSSubAlgebra of MSAlg U2 implies U1 is SubAlgebra of U2 )
assume A1: MSAlg U1 is MSSubAlgebra of MSAlg U2 ; :: thesis: U1 is SubAlgebra of U2
hence the carrier of U1 is Subset of U2 by Th13; :: according to UNIALG_2:def 7 :: thesis: for b₁ being Element of K19( the carrier of U2) holds
( not b₁ = the carrier of U1 or ( the charact of U1 = Opers (U2,b₁) & b₁ is opers_closed ) )
let B be non empty Subset of U2; :: thesis: ( not B = the carrier of U1 or ( the charact of U1 = Opers (U2,B) & B is opers_closed ) )
assume B = the carrier of U1 ; :: thesis: ( the charact of U1 = Opers (U2,B) & B is opers_closed )
hence ( the charact of U1 = Opers (U2,B) & B is opers_closed ) by A1, Th14, Th15; :: thesis: verum