:: deftheorem Def31 defines the_left_argument_of ZF_LANG:def 31 :
for H being ZF-formula st ( H is conjunctive or H is disjunctive ) holds
for b₂ being ZF-formula holds
( ( H is conjunctive implies ( b₂ = the_left_argument_of H iff ex H1 being ZF-formula st b₂ '&' H1 = H ) ) & ( not H is conjunctive implies ( b₂ = the_left_argument_of H iff ex H1 being ZF-formula st b₂ 'or' H1 = H ) ) );