:: deftheorem defines || REALSET1:def 2 :
for R being Relation
for A being set holds R || A = R | [:A,A:];