set o = the Object of C2;
take C1 --> (idm the Object of C2) ; :: thesis: ( C1 --> (idm the Object of C2) is feasible & C1 --> (idm the Object of C2) is id-preserving & ( ( C1 --> (idm the Object of C2) is Covariant & C1 --> (idm the Object of C2) is comp-preserving ) or ( C1 --> (idm the Object of C2) is Contravariant & C1 --> (idm the Object of C2) is comp-reversing ) ) )
thus ( C1 --> (idm the Object of C2) is feasible & C1 --> (idm the Object of C2) is id-preserving & ( ( C1 --> (idm the Object of C2) is Covariant & C1 --> (idm the Object of C2) is comp-preserving ) or ( C1 --> (idm the Object of C2) is Contravariant & C1 --> (idm the Object of C2) is comp-reversing ) ) ) ; :: thesis: verum