let x be set ; :: thesis: for n being Nat
for S being Language st x in (S -termsOfMaxDepth) . n holds
{ mm where mm is Element of NAT : not x in (S -termsOfMaxDepth) . mm } c= n
let n be Nat; :: thesis: for S being Language st x in (S -termsOfMaxDepth) . n holds
{ mm where mm is Element of NAT : not x in (S -termsOfMaxDepth) . mm } c= n
let S be Language; :: thesis: ( x in (S -termsOfMaxDepth) . n implies { mm where mm is Element of NAT : not x in (S -termsOfMaxDepth) . mm } c= n )
set T = S -termsOfMaxDepth ;
set A = { mm where mm is Element of NAT : not x in (S -termsOfMaxDepth) . mm } ;
assume A1: x in (S -termsOfMaxDepth) . n ; :: thesis: { mm where mm is Element of NAT : not x in (S -termsOfMaxDepth) . mm } c= n

now :: thesis: for y being object st y in { mm where mm is Element of NAT : not x in (S -termsOfMaxDepth) . mm } holds
y in Segm n

let y be object ; :: thesis: ( y in { mm where mm is Element of NAT : not x in (S -termsOfMaxDepth) . mm } implies y in Segm n )
assume y in { mm where mm is Element of NAT : not x in (S -termsOfMaxDepth) . mm } ; :: thesis: y in Segm n
then consider mm being Element of NAT such that
A2: ( y = mm & not x in (S -termsOfMaxDepth) . mm ) ;

now :: thesis: not mm >= n

assume mm >= n ; :: thesis: contradiction
then consider k being Nat such that
A3: mm = n + k by NAT_1:10;
thus contradiction by A1, A2, A3, Lm1; :: thesis: verum

end;

hence y in Segm n by A2, NAT_1:44; :: thesis: verum

end;

hence { mm where mm is Element of NAT : not x in (S -termsOfMaxDepth) . mm } c= n by TARSKI:def 3; :: thesis: verum