let R be Relation; :: thesis: for x, y being object st [x,y] in CL R holds
( x in dom (CL R) & x = y )
let x, y be object ; :: thesis: ( [x,y] in CL R implies ( x in dom (CL R) & x = y ) )
assume A1: [x,y] in CL R ; :: thesis: ( x in dom (CL R) & x = y )
then [x,y] in id (dom R) by XBOOLE_0:def 4;
hence ( x in dom (CL R) & x = y ) by A1, RELAT_1:def 10, XTUPLE_0:def 12; :: thesis: verum