let X, Y be set ; varcl ((varcl X) /\ (varcl Y)) = (varcl X) /\ (varcl Y)
set A = (varcl X) /\ (varcl Y);
now ( (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)
;
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 ;
( [x,y] in (varcl X) /\ (varcl Y) implies x c= (varcl X) /\ (varcl Y) )assume A1:
[x,y] in (varcl X) /\ (varcl Y)
;
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;
verum end;
hence
varcl ((varcl X) /\ (varcl Y)) c= (varcl X) /\ (varcl Y)
by Def1; XBOOLE_0:def 10 (varcl X) /\ (varcl Y) c= varcl ((varcl X) /\ (varcl Y))
thus
(varcl X) /\ (varcl Y) c= varcl ((varcl X) /\ (varcl Y))
by Def1; verum