set o2 = 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 reflexive )
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 reflexive ) ; :: thesis: verum