[:X,X:] c= [:X,X:] ;
hence [:X,X:] is Relation of X ; :: thesis: verum