let H be Element of QC-WFF ; :: thesis: ( H is disjunctive implies ( H is conditional & H is negative & the_argument_of H is conjunctive & the_left_argument_of (the_argument_of H) is negative & the_right_argument_of (the_argument_of H) is negative ) )
given F, G being Element of QC-WFF such that A1: H = F 'or' G ; :: according to QC_LANG2:def 10 :: thesis: ( H is conditional & H is negative & the_argument_of H is conjunctive & the_left_argument_of (the_argument_of H) is negative & the_right_argument_of (the_argument_of H) is negative )
F 'or' G = ('not' F) => G ;
hence H is conditional by A1, Def11; :: thesis: ( H is negative & the_argument_of H is conjunctive & the_left_argument_of (the_argument_of H) is negative & the_right_argument_of (the_argument_of H) is negative )
thus H is negative by A1, QC_LANG1:def 17; :: thesis: ( the_argument_of H is conjunctive & the_left_argument_of (the_argument_of H) is negative & the_right_argument_of (the_argument_of H) is negative )
A2: the_argument_of H = ('not' F) '&' ('not' G) by A1, Th2;
hence the_argument_of H is conjunctive by QC_LANG1:def 18; :: thesis: ( the_left_argument_of (the_argument_of H) is negative & the_right_argument_of (the_argument_of H) is negative )
( the_left_argument_of (the_argument_of H) = 'not' F & the_right_argument_of (the_argument_of H) = 'not' G ) by A2, Th5;
hence ( the_left_argument_of (the_argument_of H) is negative & the_right_argument_of (the_argument_of H) is negative ) by QC_LANG1:def 17; :: thesis: verum