theorem :: ORDERS_1:70

for R being Relation holds R c= [:(field R),(field R):] by Lm6;