let a, b be set ; :: thesis: ( idsym a = idsym b implies a = b )
assume idsym a = idsym b ; :: thesis: a = b
then <*a*> = <*b*> by XTUPLE_0:1;
hence a = b by Lm1; :: thesis: verum