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 A1: [x,y] in CL R ; :: thesis: [x,y] in id (dom (CL R))
then [x,y] in id (dom R) by XBOOLE_0:def 4;
then A2: x = y by RELAT_1:def 10;
x in dom (CL R) by A1, RELAT_1:20;
hence [x,y] in id (dom (CL R)) by A2, RELAT_1:def 10; :: thesis: verum

end;

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