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 VARCL;
then ( A c= varcl B & ( for x, y being set st [x,y] in varcl B holds
x c= varcl B ) ) by A1, VARCL, XBOOLE_1:1;
hence varcl A c= varcl B by VARCL; :: thesis: verum