let p, q be ZF-formula; :: thesis: ( the_left_argument_of (p 'or' q) = p & the_right_argument_of (p 'or' q) = q )
p 'or' q is disjunctive ;
then p 'or' q = (the_left_argument_of (p 'or' q)) 'or' (the_right_argument_of (p 'or' q)) by ZF_LANG:41;
hence ( the_left_argument_of (p 'or' q) = p & the_right_argument_of (p 'or' q) = q ) by ZF_LANG:31; :: thesis: verum