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 ;
B0: [:( 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 DefTruth1
.= dom ((S, the non empty set ) -TruthEval 0) by DefTruth2 ;

now

let x be set ; :: 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 B0, 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 DefFormula1; :: thesis: verum

end;

then B1: AtomicFormulasOf S c= S -formulasOfMaxDepth 0 by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in S -formulasOfMaxDepth 0 implies x in AtomicFormulasOf S )
assume x in S -formulasOfMaxDepth 0 ; :: thesis: x in AtomicFormulasOf S
then C0: x in dom (( the Element of the non empty set -InterpretersOf S,z) -TruthEval) by DefFormula1;
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 DefTruth2;
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 Lm22;
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 B0, C0, 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 by MCART_1:7; :: thesis: verum

end;

then S -formulasOfMaxDepth 0 c= AtomicFormulasOf S by TARSKI:def 3;
hence S -formulasOfMaxDepth 0 = AtomicFormulasOf S by B1, XBOOLE_0:def 10; :: thesis: verum