let A be QC-alphabet ; :: thesis: for H being Element of QC-WFF A st H is disjunctive holds
H = (the_left_disjunct_of H) 'or' (the_right_disjunct_of H)
let H be Element of QC-WFF A; :: thesis: ( H is disjunctive implies H = (the_left_disjunct_of H) 'or' (the_right_disjunct_of H) )
given F, G being Element of QC-WFF A such that A1: H = F 'or' G ; :: according to QC_LANG2:def 10 :: thesis: H = (the_left_disjunct_of H) 'or' (the_right_disjunct_of H)
the_left_disjunct_of H = F by A1, Th29;
hence H = (the_left_disjunct_of H) 'or' (the_right_disjunct_of H) by A1, Th29; :: thesis: verum