thus
( not phi is 0wff implies ex IT being set st S_{1}[IT] )
:: thesis: ( phi is 0wff implies ex b_{1} being set st b_{1} = [phi,{}] )_{1} being set st b_{1} = [phi,{}]

take IT = [phi,{}]; :: thesis: ( IT is set & IT = [phi,{}] )

thus ( IT is set & IT = [phi,{}] ) ; :: thesis: verum

proof

assume
phi is 0wff
; :: thesis: ex b
assume
not phi is 0wff
; :: thesis: ex IT being set st S_{1}[IT]

then consider m being Nat such that

A1: Depth phi = m + 1 by NAT_1:6;

end;then consider m being Nat such that

A1: Depth phi = m + 1 by NAT_1:6;

per cases
( phi is exal or not phi is exal )
;

end;

suppose
phi is exal
; :: thesis: ex IT being set st S_{1}[IT]

then
phi in m -ExFormulasOf S
by A1, Lm27;

then consider ll being Element of LettersOf S, phi0 being Element of S -formulasOfMaxDepth m such that

A2: phi = <*ll*> ^ phi0 ;

A3: ll = phi . 1 by A2, FINSEQ_1:41

.= (S -firstChar) . phi by FOMODEL0:6 ;

reconsider l = ll as literal Element of S ;

reconsider phi1 = phi0 as m -wff string of S by Def23;

reconsider IT = [phi1,{}] as set ;

take IT ; :: thesis: S_{1}[IT]

take phi1 ; :: thesis: ex p being FinSequence st

( p is AllSymbolsOf S -valued & IT = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p )

take p = {} null (AllSymbolsOf S); :: thesis: ( p is AllSymbolsOf S -valued & IT = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p )

thus p is AllSymbolsOf S -valued ; :: thesis: ( IT = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p )

thus IT = [phi1,p] ; :: thesis: phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p

thus phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p by A2, A3; :: thesis: verum

end;then consider ll being Element of LettersOf S, phi0 being Element of S -formulasOfMaxDepth m such that

A2: phi = <*ll*> ^ phi0 ;

A3: ll = phi . 1 by A2, FINSEQ_1:41

.= (S -firstChar) . phi by FOMODEL0:6 ;

reconsider l = ll as literal Element of S ;

reconsider phi1 = phi0 as m -wff string of S by Def23;

reconsider IT = [phi1,{}] as set ;

take IT ; :: thesis: S

take phi1 ; :: thesis: ex p being FinSequence st

( p is AllSymbolsOf S -valued & IT = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p )

take p = {} null (AllSymbolsOf S); :: thesis: ( p is AllSymbolsOf S -valued & IT = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p )

thus p is AllSymbolsOf S -valued ; :: thesis: ( IT = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p )

thus IT = [phi1,p] ; :: thesis: phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p

thus phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p by A2, A3; :: thesis: verum

suppose
not phi is exal
; :: thesis: ex IT being set st S_{1}[IT]

then
phi in m -NorFormulasOf S
by A1, Lm29;

then consider phi0, psi0 being Element of S -formulasOfMaxDepth m such that

A4: phi = (<*(TheNorSymbOf S)*> ^ phi0) ^ psi0 ;

A5: (S -firstChar) . phi = phi . 1 by FOMODEL0:6

.= (<*(TheNorSymbOf S)*> ^ (phi0 ^ psi0)) . 1 by A4, FINSEQ_1:32

.= TheNorSymbOf S by FINSEQ_1:41 ;

reconsider phi1 = phi0, psi1 = psi0 as m -wff string of S by Def23;

take IT = [phi1,psi0]; :: thesis: S_{1}[IT]

take phi1 ; :: thesis: ex p being FinSequence st

( p is AllSymbolsOf S -valued & IT = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p )

take p = psi1; :: thesis: ( p is AllSymbolsOf S -valued & IT = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p )

thus p is AllSymbolsOf S -valued ; :: thesis: ( IT = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p )

thus IT = [phi1,p] ; :: thesis: phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p

thus phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p by A4, A5; :: thesis: verum

end;then consider phi0, psi0 being Element of S -formulasOfMaxDepth m such that

A4: phi = (<*(TheNorSymbOf S)*> ^ phi0) ^ psi0 ;

A5: (S -firstChar) . phi = phi . 1 by FOMODEL0:6

.= (<*(TheNorSymbOf S)*> ^ (phi0 ^ psi0)) . 1 by A4, FINSEQ_1:32

.= TheNorSymbOf S by FINSEQ_1:41 ;

reconsider phi1 = phi0, psi1 = psi0 as m -wff string of S by Def23;

take IT = [phi1,psi0]; :: thesis: S

take phi1 ; :: thesis: ex p being FinSequence st

( p is AllSymbolsOf S -valued & IT = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p )

take p = psi1; :: thesis: ( p is AllSymbolsOf S -valued & IT = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p )

thus p is AllSymbolsOf S -valued ; :: thesis: ( IT = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p )

thus IT = [phi1,p] ; :: thesis: phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p

thus phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p by A4, A5; :: thesis: verum

take IT = [phi,{}]; :: thesis: ( IT is set & IT = [phi,{}] )

thus ( IT is set & IT = [phi,{}] ) ; :: thesis: verum