let x be set ; :: thesis: for m, n being Nat

for S being Language st not x in (S -termsOfMaxDepth) . (m + n) holds

not x in (S -termsOfMaxDepth) . m

let m, n be Nat; :: thesis: for S being Language st not x in (S -termsOfMaxDepth) . (m + n) holds

not x in (S -termsOfMaxDepth) . m

let S be Language; :: thesis: ( not x in (S -termsOfMaxDepth) . (m + n) implies not x in (S -termsOfMaxDepth) . m )

set T = S -termsOfMaxDepth ;

A1: (S -termsOfMaxDepth) . m c= (S -termsOfMaxDepth) . (m + n) by FOMODEL1:4;

assume not x in (S -termsOfMaxDepth) . (m + n) ; :: thesis: not x in (S -termsOfMaxDepth) . m

hence not x in (S -termsOfMaxDepth) . m by A1; :: thesis: verum

for S being Language st not x in (S -termsOfMaxDepth) . (m + n) holds

not x in (S -termsOfMaxDepth) . m

let m, n be Nat; :: thesis: for S being Language st not x in (S -termsOfMaxDepth) . (m + n) holds

not x in (S -termsOfMaxDepth) . m

let S be Language; :: thesis: ( not x in (S -termsOfMaxDepth) . (m + n) implies not x in (S -termsOfMaxDepth) . m )

set T = S -termsOfMaxDepth ;

A1: (S -termsOfMaxDepth) . m c= (S -termsOfMaxDepth) . (m + n) by FOMODEL1:4;

assume not x in (S -termsOfMaxDepth) . (m + n) ; :: thesis: not x in (S -termsOfMaxDepth) . m

hence not x in (S -termsOfMaxDepth) . m by A1; :: thesis: verum