let S be Language; :: thesis:
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),():] = 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
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:
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 (((() *) \ ),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),():] by ;
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