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