let X, Y, Z be set ; :: thesis: (X /\ Y) /\ Z = X /\ (Y /\ Z)
thus (X /\ Y) /\ Z c= X /\ (Y /\ Z) :: according to XBOOLE_0:def 10 :: thesis: X /\ (Y /\ Z) c= (X /\ Y) /\ Z

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (X /\ Y) /\ Z or x in X /\ (Y /\ Z) )
assume x in (X /\ Y) /\ Z ; :: thesis: x in X /\ (Y /\ Z)
then ( x in X /\ Y & x in Z ) by XBOOLE_0:def 4;
then ( x in X & x in Y & x in Z ) by XBOOLE_0:def 4;
then ( x in X & x in Y /\ Z ) by XBOOLE_0:def 4;
hence x in X /\ (Y /\ Z) by XBOOLE_0:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X /\ (Y /\ Z) or x in (X /\ Y) /\ Z )
assume x in X /\ (Y /\ Z) ; :: thesis: x in (X /\ Y) /\ Z
then ( x in X & x in Y /\ Z ) by XBOOLE_0:def 4;
then ( x in X & x in Y & x in Z ) by XBOOLE_0:def 4;
then ( x in X /\ Y & x in Z ) by XBOOLE_0:def 4;
hence x in (X /\ Y) /\ Z by XBOOLE_0:def 4; :: thesis: verum