reconsider mm = m as Element of NAT by ORDINAL1:def 12;
set SS = AllSymbolsOf S;
set Phim = S -formulasOfMaxDepth m;
defpred S₁[ 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₁[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 )

proof

assume A1: x = S -formulasOfMaxDepth m ; :: thesis: S₁[x]
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;

end;

assume A2: S₁[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