theorem :: FUNCT_1:22

for X, Y being set holds (id X) * (id Y) = id (X /\ Y)