let x, y be set ; :: thesis: for R being Relation st [x,y] in CL R holds
( x in dom (CL R) & x = y )
let R be Relation; :: 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:20, RELAT_1:def 10; :: thesis: verum