thus Non a is negative :: thesis: not Non a is positive
proof
take a ; :: according to ABCMIZ_1:def 38 :: thesis: ( a is positive & Non a = (non_op C) term a )
thus ( a is positive & Non a = (non_op C) term a ) by Th59; :: thesis: verum
end;
take a ; :: according to ABCMIZ_1:def 37 :: thesis: Non a = (non_op C) term a
thus Non a = (non_op C) term a by Th59; :: thesis: verum