take Imf X,X ; :: thesis: ( Imf X,X is reflexive & Imf X,X is transitive & Imf X,X is symmetric & Imf X,X is antisymmetric )
thus ( Imf X,X is reflexive & Imf X,X is transitive & Imf X,X is symmetric & Imf X,X is antisymmetric ) ; :: thesis: verum