A1: for x, y being set st [x,y] in {} holds
x c= {} ;
for B being set st {} c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
{} c= B ;
hence varcl {} = {} by A1, Def1; :: thesis: verum