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 )

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 ) ; :: thesis: verum

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 )

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 ) ; :: thesis: verum