let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds Union the Sorts of T = union { (T deg<= i) where i is Nat : verum }
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds Union the Sorts of T = union { (T deg<= i) where i is Nat : verum }
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: Union the Sorts of T = union { (T deg<= i) where i is Nat : verum }
thus Union the Sorts of T c= union { (T deg<= i) where i is Nat : verum } :: according to XBOOLE_0:def 10 :: thesis: union { (T deg<= i) where i is Nat : verum } c= Union the Sorts of T

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Union the Sorts of T or a in union { (T deg<= i) where i is Nat : verum } )
assume a in Union the Sorts of T ; :: thesis: a in union { (T deg<= i) where i is Nat : verum }
then reconsider t = a as Element of T ;
( t in T deg<= (deg t) & T deg<= (deg t) in { (T deg<= i) where i is Nat : verum } ) ;
hence a in union { (T deg<= i) where i is Nat : verum } by TARSKI:def 4; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { (T deg<= i) where i is Nat : verum } or a in Union the Sorts of T )
assume a in union { (T deg<= i) where i is Nat : verum } ; :: thesis: a in Union the Sorts of T
then consider I being set such that
A1: ( a in I & I in { (T deg<= i) where i is Nat : verum } ) by TARSKI:def 4;
consider i being Nat such that
A2: I = T deg<= i by A1;
thus a in Union the Sorts of T by A1, A2; :: thesis: verum