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