let i, j be Nat; :: thesis: for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S st i <= j holds
T deg<= i c= T deg<= j
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 st i <= j holds
T deg<= i c= T deg<= j
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 st i <= j holds
T deg<= i c= T deg<= j
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: ( i <= j implies T deg<= i c= T deg<= j )
assume Z0: i <= j ; :: thesis: T deg<= i c= T deg<= j
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in T deg<= i or a in T deg<= j )
assume a in T deg<= i ; :: thesis: a in T deg<= j
then consider r being Element of T such that
A2: ( a = r & deg r <= i ) ;
deg r <= j by Z0, A2, XXREAL_0:2;
hence a in T deg<= j by A2; :: thesis: verum