reconsider mm = m as Element of NAT by ORDINAL1:def 12;

set SS = AllSymbolsOf S;

set Phim = S -formulasOfMaxDepth m;

defpred S_{1}[ set ] means for U being non empty set

for I being Element of U -InterpretersOf S holds $1 = dom ((I,m) -TruthEval);

let x be Subset of (((AllSymbolsOf S) *) \ {{}}); :: thesis: ( x = S -formulasOfMaxDepth m iff for U being non empty set

for I being Element of U -InterpretersOf S holds x = dom ((I,m) -TruthEval) )

thus ( x = S -formulasOfMaxDepth m implies S_{1}[x] )
:: thesis: ( ( for U being non empty set

for I being Element of U -InterpretersOf S holds x = dom ((I,m) -TruthEval) ) implies x = S -formulasOfMaxDepth m )_{1}[x]
; :: thesis: x = S -formulasOfMaxDepth m

for U being non empty set

for I being Element of U -InterpretersOf S

for nn being Element of NAT st m = nn holds

x = dom ((I,nn) -TruthEval) by A2;

hence x = S -formulasOfMaxDepth m by Def22; :: thesis: verum

set SS = AllSymbolsOf S;

set Phim = S -formulasOfMaxDepth m;

defpred S

for I being Element of U -InterpretersOf S holds $1 = dom ((I,m) -TruthEval);

let x be Subset of (((AllSymbolsOf S) *) \ {{}}); :: thesis: ( x = S -formulasOfMaxDepth m iff for U being non empty set

for I being Element of U -InterpretersOf S holds x = dom ((I,m) -TruthEval) )

thus ( x = S -formulasOfMaxDepth m implies S

for I being Element of U -InterpretersOf S holds x = dom ((I,m) -TruthEval) ) implies x = S -formulasOfMaxDepth m )

proof

assume A2:
S
assume A1:
x = S -formulasOfMaxDepth m
; :: thesis: S_{1}[x]

thus for U being non empty set

for I being Element of U -InterpretersOf S holds x = dom ((I,m) -TruthEval) :: thesis: verum

end;thus for U being non empty set

for I being Element of U -InterpretersOf S holds x = dom ((I,m) -TruthEval) :: thesis: verum

proof

let U be non empty set ; :: thesis: for I being Element of U -InterpretersOf S holds x = dom ((I,m) -TruthEval)

set II = U -InterpretersOf S;

let I be Element of U -InterpretersOf S; :: thesis: x = dom ((I,m) -TruthEval)

S -formulasOfMaxDepth m = dom ((I,mm) -TruthEval) by Def22;

hence x = dom ((I,m) -TruthEval) by A1; :: thesis: verum

end;set II = U -InterpretersOf S;

let I be Element of U -InterpretersOf S; :: thesis: x = dom ((I,m) -TruthEval)

S -formulasOfMaxDepth m = dom ((I,mm) -TruthEval) by Def22;

hence x = dom ((I,m) -TruthEval) by A1; :: thesis: verum

for U being non empty set

for I being Element of U -InterpretersOf S

for nn being Element of NAT st m = nn holds

x = dom ((I,nn) -TruthEval) by A2;

hence x = S -formulasOfMaxDepth m by Def22; :: thesis: verum