let C be initialized ConstructorSignature; :: thesis: for a1, a2 being quasi-adjective of C st Non a1 = Non a2 holds
a1 = a2
let a1, a2 be quasi-adjective of C; :: thesis: ( Non a1 = Non a2 implies a1 = a2 )
( Non (Non a1) = a1 & Non (Non a2) = a2 ) by Th46;
hence ( Non a1 = Non a2 implies a1 = a2 ) ; :: thesis: verum