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 by Th67;
hence ( Non a1 = Non a2 implies a1 = a2 ) by Th67; :: thesis: verum