let X be set ; :: thesis: (id X) ~ = id X
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b being set holds
( [x,b] in (id X) ~ iff [x,b] in id X )
let y be set ; :: thesis: ( [x,y] in (id X) ~ iff [x,y] in id X )
thus ( [x,y] in (id X) ~ implies [x,y] in id X ) :: thesis: ( [x,y] in id X implies [x,y] in (id X) ~ )

proof

assume [x,y] in (id X) ~ ; :: thesis: [x,y] in id X
then [y,x] in id X by Def7;
hence [x,y] in id X by Def10; :: thesis: verum

end;

assume A1: [x,y] in id X ; :: thesis: [x,y] in (id X) ~
then x = y by Def10;
hence [x,y] in (id X) ~ by A1, Def7; :: thesis: verum