thus ( not phi is 0wff implies ex IT being set st S₁[IT] ) :: thesis: ( phi is 0wff implies ex b₁ being set st b₁ = [phi,{}] )

proof

assume not phi is 0wff ; :: thesis: ex IT being set st S₁[IT]
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 ) ;

suppose phi is exal ; :: thesis: ex IT being set st S₁[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₁[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;

suppose not phi is exal ; :: thesis: ex IT being set st S₁[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₁[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;

end;

end;

assume phi is 0wff ; :: thesis: ex b₁ being set st b₁ = [phi,{}]
take IT = [phi,{}]; :: thesis: ( IT is set & IT = [phi,{}] )
thus ( IT is set & IT = [phi,{}] ) ; :: thesis: verum