let S be Language; :: thesis: S -formulasOfMaxDepth 0 = AtomicFormulasOf S
set U = the non empty set ;
set AF = AtomicFormulasOf S;
set II = the non empty set -InterpretersOf S;
set I = the Element of the non empty set -InterpretersOf S;
reconsider z = 0 as Element of NAT ;
A1: [:( the non empty set -InterpretersOf S),(AtomicFormulasOf S):] = dom (S -TruthEval the non empty set ) by FUNCT_2:def 1
.= dom (((S, the non empty set ) -TruthEval) . z) by Def19
.= dom ((S, the non empty set ) -TruthEval 0) by Def20 ;

now :: thesis: for x being object st x in AtomicFormulasOf S holds
x in S -formulasOfMaxDepth 0

let x be object ; :: thesis: ( x in AtomicFormulasOf S implies x in S -formulasOfMaxDepth 0 )
assume x in AtomicFormulasOf S ; :: thesis: x in S -formulasOfMaxDepth 0
then [ the Element of the non empty set -InterpretersOf S,x] in dom ((S, the non empty set ) -TruthEval 0) by A1, ZFMISC_1:def 2;
then x in dom (( the Element of the non empty set -InterpretersOf S,z) -TruthEval) by FUNCT_5:20;
hence x in S -formulasOfMaxDepth 0 by Def22; :: thesis: verum

end;

then A2: AtomicFormulasOf S c= S -formulasOfMaxDepth 0 ;

now :: thesis: for x being object st x in S -formulasOfMaxDepth 0 holds
x in AtomicFormulasOf S

let x be object ; :: thesis: ( x in S -formulasOfMaxDepth 0 implies x in AtomicFormulasOf S )
assume x in S -formulasOfMaxDepth 0 ; :: thesis: x in AtomicFormulasOf S
then A3: x in dom (( the Element of the non empty set -InterpretersOf S,z) -TruthEval) by Def22;
set f = (S, the non empty set ) -TruthEval z;
set g = ( the Element of the non empty set -InterpretersOf S,z) -TruthEval ;
(S, the non empty set ) -TruthEval z = ((S, the non empty set ) -TruthEval) . z by Def20;
then reconsider gg = curry ((S, the non empty set ) -TruthEval z) as Function of ( the non empty set -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN)) by Lm10;
dom gg = the non empty set -InterpretersOf S by FUNCT_2:def 1;
then [ the Element of the non empty set -InterpretersOf S,x] in [:( the non empty set -InterpretersOf S),(AtomicFormulasOf S):] by A1, A3, FUNCT_5:31;
then [ the Element of the non empty set -InterpretersOf S,x] `2 in AtomicFormulasOf S by MCART_1:10;
hence x in AtomicFormulasOf S ; :: thesis: verum

end;

then S -formulasOfMaxDepth 0 c= AtomicFormulasOf S ;
hence S -formulasOfMaxDepth 0 = AtomicFormulasOf S by A2; :: thesis: verum