thus ( not phi is 0wff implies ex IT being set st S1[IT] ) :: thesis: ( phi is 0wff implies ex b1 being set st b1 = [phi,{}] )
proof
assume not phi is 0wff ; :: thesis: ex IT being set st S1[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 S1[IT]
then phi in m -ExFormulasOf S by ;
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
.= () . 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: S1[IT]
take phi1 ; :: thesis: ex p being FinSequence st
( p is AllSymbolsOf S -valued & IT = [phi1,p] & phi = (<*(() . phi)*> ^ phi1) ^ p )

take p = {} null (); :: thesis: ( p is AllSymbolsOf S -valued & IT = [phi1,p] & phi = (<*(() . phi)*> ^ phi1) ^ p )
thus p is AllSymbolsOf S -valued ; :: thesis: ( IT = [phi1,p] & phi = (<*(() . phi)*> ^ phi1) ^ p )
thus IT = [phi1,p] ; :: thesis: phi = (<*(() . phi)*> ^ phi1) ^ p
thus phi = (<*(() . phi)*> ^ phi1) ^ p by A2, A3; :: thesis: verum
end;
suppose not phi is exal ; :: thesis: ex IT being set st S1[IT]
then phi in m -NorFormulasOf S by ;
then consider phi0, psi0 being Element of S -formulasOfMaxDepth m such that
A4: phi = (<*()*> ^ phi0) ^ psi0 ;
A5: () . phi = phi . 1 by FOMODEL0:6
.= (<*()*> ^ (phi0 ^ psi0)) . 1 by
.= TheNorSymbOf S by FINSEQ_1:41 ;
reconsider phi1 = phi0, psi1 = psi0 as m -wff string of S by Def23;
take IT = [phi1,psi0]; :: thesis: S1[IT]
take phi1 ; :: thesis: ex p being FinSequence st
( p is AllSymbolsOf S -valued & IT = [phi1,p] & phi = (<*(() . phi)*> ^ phi1) ^ p )

take p = psi1; :: thesis: ( p is AllSymbolsOf S -valued & IT = [phi1,p] & phi = (<*(() . phi)*> ^ phi1) ^ p )
thus p is AllSymbolsOf S -valued ; :: thesis: ( IT = [phi1,p] & phi = (<*(() . phi)*> ^ phi1) ^ p )
thus IT = [phi1,p] ; :: thesis: phi = (<*(() . phi)*> ^ phi1) ^ p
thus phi = (<*(() . phi)*> ^ phi1) ^ p by A4, A5; :: thesis: verum
end;
end;
end;
assume phi is 0wff ; :: thesis: ex b1 being set st b1 = [phi,{}]
take IT = [phi,{}]; :: thesis: ( IT is set & IT = [phi,{}] )
thus ( IT is set & IT = [phi,{}] ) ; :: thesis: verum