theorem :: ZF_LANG1:24

for H being ZF-formula st H is disjunctive holds
the_right_argument_of H = the_argument_of (the_right_argument_of (the_argument_of H))