let H be ZF-formula; :: thesis: for x, y being Variable st H is negative holds
the_argument_of (H / x,y) = (the_argument_of H) / x,y
let x, y be Variable; :: thesis: ( H is negative implies the_argument_of (H / x,y) = (the_argument_of H) / x,y )
assume A1: H is negative ; :: thesis: the_argument_of (H / x,y) = (the_argument_of H) / x,y
then H / x,y is negative by Th182;
then A2: H / x,y = 'not' (the_argument_of (H / x,y)) by ZF_LANG:def 30;
H = 'not' (the_argument_of H) by A1, ZF_LANG:def 30;
hence the_argument_of (H / x,y) = (the_argument_of H) / x,y by A2, Th170; :: thesis: verum