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

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

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

end;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

hence
y in Segm n
by A2, NAT_1:44; :: thesis: verumassume
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;then consider k being Nat such that

A3: mm = n + k by NAT_1:10;

thus contradiction by A1, A2, A3, Lm1; :: thesis: verum