let R be Relation; :: thesis: ( R c= id (dom R) implies R = id (dom R) )
assume A1: R c= id (dom R) ; :: thesis: R = id (dom R)
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in R or [x,y] in id (dom R) ) & ( not [x,y] in id (dom R) or [x,y] in R ) )
thus ( [x,y] in R implies [x,y] in id (dom R) ) by A1; :: thesis: ( not [x,y] in id (dom R) or [x,y] in R )
assume A2: [x,y] in id (dom R) ; :: thesis: [x,y] in R
then x in dom R by RELAT_1:def 10;
then A3: ex z being object st [x,z] in R by XTUPLE_0:def 12;
x = y by A2, RELAT_1:def 10;
hence [x,y] in R by A1, A3, RELAT_1:def 10; :: thesis: verum