let S be Language; 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
;
then A2:
AtomicFormulasOf S c= S -formulasOfMaxDepth 0
;
now for x being object st x in S -formulasOfMaxDepth 0 holds
x in AtomicFormulasOf Slet x be
object ;
( x in S -formulasOfMaxDepth 0 implies x in AtomicFormulasOf S )assume
x in S -formulasOfMaxDepth 0
;
x in AtomicFormulasOf Sthen 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
;
verum end;
then
S -formulasOfMaxDepth 0 c= AtomicFormulasOf S
;
hence
S -formulasOfMaxDepth 0 = AtomicFormulasOf S
by A2; verum