let A, B be set ; :: thesis: ( A c= B implies varcl A c= varcl B )
assume A1: A c= B ; :: thesis: varcl A c= varcl B
B c= varcl B by Def1;
then A2: A c= varcl B by A1;
for x, y being set st [x,y] in varcl B holds
x c= varcl B by Def1;
hence varcl A c= varcl B by A2, Def1; :: thesis: verum