let x, y be object ; :: thesis: for R being Relation holds
( ( R * R = R & R * (R \ (id (dom R))) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) & ( R * R = R & (R \ (id (dom R))) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) )
let R be Relation; :: thesis: ( ( R * R = R & R * (R \ (id (dom R))) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) & ( R * R = R & (R \ (id (dom R))) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) )
R \ (CL R) = R \ (id (dom R)) by XBOOLE_1:47;
hence ( ( R * R = R & R * (R \ (id (dom R))) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) & ( R * R = R & (R \ (id (dom R))) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) ) by Th29; :: thesis: verum