theorem :: ZF_LANG1:23

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