set o2 = the Object of C2;
take C1 --> (idm the Object of C2) ; :: thesis: ( C1 --> (idm the Object of C2) is id-preserving & C1 --> (idm the Object of C2) is feasible & C1 --> (idm the Object of C2) is reflexive & C1 --> (idm the Object of C2) is strict )
thus ( C1 --> (idm the Object of C2) is id-preserving & C1 --> (idm the Object of C2) is feasible & C1 --> (idm the Object of C2) is reflexive & C1 --> (idm the Object of C2) is strict ) ; :: thesis: verum