take [:X,X:] ; :: thesis: ( [:X,X:] is Relation of X & not [:X,X:] is antisymmetric )
[:X,X:] c= [:X,X:] ;
hence ( [:X,X:] is Relation of X & not [:X,X:] is antisymmetric ) ; :: thesis: verum