theorem Th40: :: ZF_LANG:40

for H being ZF-formula st H is conjunctive holds
H = (the_left_argument_of H) '&' (the_right_argument_of H)