:: deftheorem Def34 defines SubWffsOf FOMODEL2:def 35 :
for S being Language
for phi being wff string of S
for b₃ being set holds
( ( not phi is 0wff implies ( b₃ = SubWffsOf phi iff ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued & b₃ = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) ) ) & ( phi is 0wff implies ( b₃ = SubWffsOf phi iff b₃ = [phi,{}] ) ) );