let X, Y be set ; :: thesis: varcl ((varcl X) /\ (varcl Y)) = (varcl X) /\ (varcl Y)
set A = (varcl X) /\ (varcl Y);
now :: thesis: ( (varcl X) /\ (varcl Y) c= (varcl X) /\ (varcl Y) & ( for x, y being set st [x,y] in (varcl X) /\ (varcl Y) holds
x c= (varcl X) /\ (varcl Y) ) )
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 A1: [x,y] in (varcl X) /\ (varcl Y) ; :: thesis: x c= (varcl X) /\ (varcl Y)
then A2: [x,y] in varcl X by XBOOLE_0:def 4;
A3: [x,y] in varcl Y by A1, XBOOLE_0:def 4;
A4: x c= varcl X by A2, Def1;
x c= varcl Y by A3, Def1;
hence x c= (varcl X) /\ (varcl Y) by A4, XBOOLE_1:19; :: thesis: verum
end;
hence varcl ((varcl X) /\ (varcl Y)) c= (varcl X) /\ (varcl Y) by Def1; :: 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 Def1; :: thesis: verum