let A be non empty set ; :: thesis: R5(A,A)
thus not A misses A ; :: thesis: verum