theorem :: ZF_LANG:41

for H being ZF-formula st H is disjunctive holds
H = (the_left_argument_of H) 'or' (the_right_argument_of H)