let R be Relation; :: thesis: ( (id (field R)) * R = R & R * (id (field R)) = R )
( dom R c= field R & rng R c= field R ) by XBOOLE_1:7;
hence ( (id (field R)) * R = R & R * (id (field R)) = R ) by RELAT_1:51, RELAT_1:53; :: thesis: verum