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

assume A5: x in X /\ (Y /\ Z) ; :: thesis: x in (X /\ Y) /\ Z

then A6: x in Y /\ Z by XBOOLE_0:def 4;

then A7: x in Y by XBOOLE_0:def 4;

A8: x in Z by A6, XBOOLE_0:def 4;

x in X by A5, XBOOLE_0:def 4;

then x in X /\ Y by A7, XBOOLE_0:def 4;

hence x in (X /\ Y) /\ Z by A8, XBOOLE_0:def 4; :: thesis: verum

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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in X /\ (Y /\ Z) or x in (X /\ Y) /\ Z )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (X /\ Y) /\ Z or x in X /\ (Y /\ Z) )

assume A1: x in (X /\ Y) /\ Z ; :: thesis: x in X /\ (Y /\ Z)

then A2: x in Z by XBOOLE_0:def 4;

A3: x in X /\ Y by A1, XBOOLE_0:def 4;

then A4: x in X by XBOOLE_0:def 4;

x in Y by A3, XBOOLE_0:def 4;

then x in Y /\ Z by A2, XBOOLE_0:def 4;

hence x in X /\ (Y /\ Z) by A4, XBOOLE_0:def 4; :: thesis: verum

end;assume A1: x in (X /\ Y) /\ Z ; :: thesis: x in X /\ (Y /\ Z)

then A2: x in Z by XBOOLE_0:def 4;

A3: x in X /\ Y by A1, XBOOLE_0:def 4;

then A4: x in X by XBOOLE_0:def 4;

x in Y by A3, XBOOLE_0:def 4;

then x in Y /\ Z by A2, XBOOLE_0:def 4;

hence x in X /\ (Y /\ Z) by A4, XBOOLE_0:def 4; :: thesis: verum

assume A5: x in X /\ (Y /\ Z) ; :: thesis: x in (X /\ Y) /\ Z

then A6: x in Y /\ Z by XBOOLE_0:def 4;

then A7: x in Y by XBOOLE_0:def 4;

A8: x in Z by A6, XBOOLE_0:def 4;

x in X by A5, XBOOLE_0:def 4;

then x in X /\ Y by A7, XBOOLE_0:def 4;

hence x in (X /\ Y) /\ Z by A8, XBOOLE_0:def 4; :: thesis: verum