let C be initialized ConstructorSignature; :: thesis: for a being quasi-adjective of C holds Non a <> a
let a be quasi-adjective of C; :: thesis: Non a <> a

per cases ( a is positive or a is negative ) ;

suppose a is positive ; :: thesis: Non a <> a

then reconsider a9 = a as positive quasi-adjective of C ;
Non a9 is negative quasi-adjective of C ;
hence Non a <> a ; :: thesis: verum

end;

suppose a is negative ; :: thesis: Non a <> a

then reconsider a9 = a as negative quasi-adjective of C ;
Non a9 is positive quasi-adjective of C ;
hence Non a <> a ; :: thesis: verum

end;

end;