let x be set ; :: thesis: for S being Language st x in AllTermsOf S holds
ex nn being Element of NAT st x in (S -termsOfMaxDepth) . nn
let S be Language; :: thesis: ( x in AllTermsOf S implies ex nn being Element of NAT st x in (S -termsOfMaxDepth) . nn )
set T = S -termsOfMaxDepth ;
assume x in AllTermsOf S ; :: thesis: ex nn being Element of NAT st x in (S -termsOfMaxDepth) . nn
then consider Y being set such that
A1: ( x in Y & Y in rng (S -termsOfMaxDepth) ) by TARSKI:def 4;
consider mmm being object such that
A2: ( mmm in dom (S -termsOfMaxDepth) & Y = (S -termsOfMaxDepth) . mmm ) by A1, FUNCT_1:def 3;
reconsider mm = mmm as Element of NAT by A2, Def30;
take nn = mm; :: thesis: x in (S -termsOfMaxDepth) . nn
thus x in (S -termsOfMaxDepth) . nn by A1, A2; :: thesis: verum