let t be GRZ-formula; :: thesis: ( t is negative iff ex u being GRZ-formula st t = 'not' u )
thus ( t is negative implies ex u being GRZ-formula st t = 'not' u ) :: thesis: ( ex u being GRZ-formula st t = 'not' u implies t is negative )
proof
assume t is negative ; :: thesis: ex u being GRZ-formula st t = 'not' u
then consider u being GRZ-formula such that
A3: t = (Polish-unOp (GRZ-symbols,GRZ-arity,'not')) . u by Th4, POLNOT_1:80;
take u ; :: thesis: t = 'not' u
thus t = 'not' u by A3; :: thesis: verum
end;
thus ( ex u being GRZ-formula st t = 'not' u implies t is negative ) by Th4, POLNOT_1:81; :: thesis: verum