let X, Y, Z be set ; :: thesis: X /\ (Y /\ Z) = (X /\ Y) /\ (X /\ Z)
thus X /\ (Y /\ Z) = ((X /\ X) /\ Y) /\ Z by Th16
.= (X /\ (X /\ Y)) /\ Z by Th16
.= (X /\ Y) /\ (X /\ Z) by Th16 ; :: thesis: verum