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