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