let X, Y be set ; :: thesis: varcl ((varcl X) /\ (varcl Y)) = (varcl X) /\ (varcl Y)
set A = (varcl X) /\ (varcl Y);

now

thus (varcl X) /\ (varcl Y) c= (varcl X) /\ (varcl Y) ; :: thesis: for x, y being set st [x,y] in (varcl X) /\ (varcl Y) holds
x c= (varcl X) /\ (varcl Y)
let x, y be set ; :: thesis: ( [x,y] in (varcl X) /\ (varcl Y) implies x c= (varcl X) /\ (varcl Y) )
assume [x,y] in (varcl X) /\ (varcl Y) ; :: thesis: x c= (varcl X) /\ (varcl Y)
then ( [x,y] in varcl X & [x,y] in varcl Y ) by XBOOLE_0:def 4;
then ( x c= varcl X & x c= varcl Y ) by VARCL;
hence x c= (varcl X) /\ (varcl Y) by XBOOLE_1:19; :: thesis: verum

end;

hence varcl ((varcl X) /\ (varcl Y)) c= (varcl X) /\ (varcl Y) by VARCL; :: according to XBOOLE_0:def 10 :: thesis: (varcl X) /\ (varcl Y) c= varcl ((varcl X) /\ (varcl Y))
thus (varcl X) /\ (varcl Y) c= varcl ((varcl X) /\ (varcl Y)) by VARCL; :: thesis: verum