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

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