let A be non empty set ; :: thesis: R5(A,A)
ex x being set st x in A by XBOOLE_0:def 1;
hence R5(A,A) by XBOOLE_0:3; :: thesis: verum