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;