let F, H be ZF-formula; :: thesis: ( H is disjunctive implies ( ( F = the_left_argument_of H implies ex G being ZF-formula st F 'or' G = H ) & ( ex G being ZF-formula st F 'or' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G 'or' F = H ) & ( ex G being ZF-formula st G 'or' F = H implies F = the_right_argument_of H ) ) )
assume A1: H is disjunctive ; :: thesis: ( ( F = the_left_argument_of H implies ex G being ZF-formula st F 'or' G = H ) & ( ex G being ZF-formula st F 'or' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G 'or' F = H ) & ( ex G being ZF-formula st G 'or' F = H implies F = the_right_argument_of H ) )
then ex F, G being ZF-formula st H = F 'or' G ;
then H . 1 = 2 by FINSEQ_1:41;
then not H is conjunctive by Th21;
hence ( ( F = the_left_argument_of H implies ex G being ZF-formula st F 'or' G = H ) & ( ex G being ZF-formula st F 'or' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G 'or' F = H ) & ( ex G being ZF-formula st G 'or' F = H implies F = the_right_argument_of H ) ) by A1, Def31, Def32; :: thesis: verum