let H be ZF-formula; :: thesis: ( H is disjunctive implies H = (the_left_argument_of H) 'or' (the_right_argument_of H) )
assume A1: H is disjunctive ; :: thesis: H = (the_left_argument_of H) 'or' (the_right_argument_of H)
then ex F1 being ZF-formula st H = (the_left_argument_of H) 'or' F1 by Th39;
hence H = (the_left_argument_of H) 'or' (the_right_argument_of H) by A1, Th39; :: thesis: verum