let X be set ; :: thesis: (id X) ~ = id X
for x, y being set holds
( [x,y] in (id X) ~ iff [x,y] in id X )

proof

let x, 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;

thus ( [x,y] in id X implies [x,y] in (id X) ~ ) :: thesis: verum

proof

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

end;

end;

hence (id X) ~ = id X by Def2; :: thesis: verum