set o = the Object of C2;
set m = the Morphism of the Object of C2, the Object of C2;
take C1 --> the Morphism of the Object of C2, the Object of C2 ; :: thesis: ( C1 --> the Morphism of the Object of C2, the Object of C2 is feasible & C1 --> the Morphism of the Object of C2, the Object of C2 is Covariant & C1 --> the Morphism of the Object of C2, the Object of C2 is Contravariant )
thus ( C1 --> the Morphism of the Object of C2, the Object of C2 is feasible & C1 --> the Morphism of the Object of C2, the Object of C2 is Covariant & C1 --> the Morphism of the Object of C2, the Object of C2 is Contravariant ) ; :: thesis: verum