theorem :: ORDERS_1:84

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