let j be Element of NAT ; :: thesis: for A being Subset of Vars holds varcl {[(varcl A),j]} = (varcl A) \/ {[(varcl A),j]}
let A be Subset of Vars; :: thesis: varcl {[(varcl A),j]} = (varcl A) \/ {[(varcl A),j]}
A1: {[(varcl A),j]} c= (varcl A) \/ {[(varcl A),j]} by XBOOLE_1:7;
A2: varcl A c= (varcl A) \/ {[(varcl A),j]} by XBOOLE_1:7;
now :: thesis: for x, y being set st [x,y] in (varcl A) \/ {[(varcl A),j]} holds
x c= (varcl A) \/ {[(varcl A),j]}
let x, y be set ; :: thesis: ( [x,y] in (varcl A) \/ {[(varcl A),j]} implies x c= (varcl A) \/ {[(varcl A),j]} )
assume [x,y] in (varcl A) \/ {[(varcl A),j]} ; :: thesis: x c= (varcl A) \/ {[(varcl A),j]}
then ( [x,y] in varcl A or [x,y] in {[(varcl A),j]} ) by XBOOLE_0:def 3;
then ( [x,y] in varcl A or [x,y] = [(varcl A),j] ) by TARSKI:def 1;
then ( x c= varcl A or x = varcl A ) by Def1, XTUPLE_0:1;
hence x c= (varcl A) \/ {[(varcl A),j]} by A2; :: thesis: verum
end;
hence varcl {[(varcl A),j]} c= (varcl A) \/ {[(varcl A),j]} by A1, Def1; :: according to XBOOLE_0:def 10 :: thesis: (varcl A) \/ {[(varcl A),j]} c= varcl {[(varcl A),j]}
A3: {[(varcl A),j]} c= varcl {[(varcl A),j]} by Def1;
[(varcl A),j] in {[(varcl A),j]} by TARSKI:def 1;
then varcl A c= varcl {[(varcl A),j]} by A3, Def1;
hence (varcl A) \/ {[(varcl A),j]} c= varcl {[(varcl A),j]} by A3, XBOOLE_1:8; :: thesis: verum