let R be Relation; :: thesis: CL R = id (dom (CL R))
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [x,b₁] in CL R or [x,b₁] in id (dom (CL R)) ) & ( not [x,b₁] in id (dom (CL R)) or [x,b₁] in CL R ) )
let y be set ; :: thesis: ( ( not [x,y] in CL R or [x,y] in id (dom (CL R)) ) & ( not [x,y] in id (dom (CL R)) or [x,y] in CL R ) )
thus ( [x,y] in CL R implies [x,y] in id (dom (CL R)) ) :: thesis: ( not [x,y] in id (dom (CL R)) or [x,y] in CL R )

proof

assume [x,y] in CL R ; :: thesis: [x,y] in id (dom (CL R))
then ( x in dom (CL R) & [x,y] in id (dom R) ) by RELAT_1:20, XBOOLE_0:def 4;
then ( x in dom (CL R) & x = y ) by RELAT_1:def 10;
hence [x,y] in id (dom (CL R)) by RELAT_1:def 10; :: thesis: verum

end;

assume [x,y] in id (dom (CL R)) ; :: thesis: [x,y] in CL R
then A1: ( x in dom (CL R) & x = y ) by RELAT_1:def 10;
then ex z being set st [x,z] in CL R by RELAT_1:def 4;
hence [x,y] in CL R by A1, Th44; :: thesis: verum