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 Th168;
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, Th156; :: thesis: verum