let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra over S
for A being MSSubset of U0 holds SubSort A c= SubSort U0
let U0 be MSAlgebra over S; :: thesis: for A being MSSubset of U0 holds SubSort A c= SubSort U0
let A be MSSubset of U0; :: thesis: SubSort A c= SubSort U0
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SubSort A or x in SubSort U0 )
assume A1: x in SubSort A ; :: thesis: x in SubSort U0
A2: for B being MSSubset of U0 st B = x holds
B is opers_closed by A1, Def10;
( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 ) by A1, Def10;
hence x in SubSort U0 by A2, Def11; :: thesis: verum