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