x in {x} by TARSKI:def 1;
hence {[x,x]} is Relation of {x} by RELSET_1:3; :: thesis: verum