let x be non pair set ; :: thesis: for R being Relation holds not x in R
for a, b being object holds not x = [a,b] ;
hence for R being Relation holds not x in R by RELAT_1:def 1; :: thesis: verum