let H be Element of QC-WFF ; :: thesis: ( H is conjunctive implies Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} )
assume H is conjunctive ; :: thesis: Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}
then H = (the_left_argument_of H) '&' (the_right_argument_of H) by Th4;
hence Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} by Th111; :: thesis: verum