take canonical_homomorphism T ; :: thesis: canonical_homomorphism T is x -constant
thus canonical_homomorphism T is x -constant by Th51; :: thesis: verum