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

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