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