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 be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [x,b₁] in R or [x,b₁] in id (dom R) ) & ( not [x,b₁] in id (dom R) or [x,b₁] in R ) )
let y be set ; :: 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 [x,y] in id (dom R) ; :: thesis: [x,y] in R
then A2: ( x in dom R & x = y ) by RELAT_1:def 10;
then consider z being set such that
A3: [x,z] in R by RELAT_1:def 4;
thus [x,y] in R by A1, A2, A3, RELAT_1:def 10; :: thesis: verum