set u = the Element of V;
take [: the Element of V, the Element of V:] ; :: thesis: [: the Element of V, the Element of V:] is Relation-like
thus [: the Element of V, the Element of V:] is Relation-like ; :: thesis: verum