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 B0: x in (S -termsOfMaxDepth) . n ; :: thesis: { mm where mm is Element of NAT : not x in (S -termsOfMaxDepth) . mm } c= n

now

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

now

assume mm >= n ; :: thesis: contradiction
then consider k being Nat such that
D0: mm = n + k by NAT_1:10;
thus contradiction by B0, C0, D0, Lm2; :: thesis: verum

end;

hence y in n by C0, 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