:: deftheorem Def1 defines list_of_immediate_constituents QC_LANG4:def 1 :
for A being QC-alphabet
for p being Element of QC-WFF A holds
( ( ( p = VERUM A or p is atomic ) implies list_of_immediate_constituents p = <*> (QC-WFF A) ) & ( p is negative implies list_of_immediate_constituents p = <*(the_argument_of p)*> ) & ( p is conjunctive implies list_of_immediate_constituents p = <*(the_left_argument_of p),(the_right_argument_of p)*> ) & ( p = VERUM A or p is atomic or p is negative or p is conjunctive or list_of_immediate_constituents p = <*(the_scope_of p)*> ) );