theorem :: LANG1:18

for R being Relation holds R c= R [*]