for R being Relation holds R |_2 {} = {} by Lm17;