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 x in X \/ (Y \/ Z) ; :: thesis: x in (X \/ Y) \/ Z

then ( x in X or x in Y \/ Z ) by XBOOLE_0:def 3;

then ( x in X or x in Y or x in Z ) by XBOOLE_0:def 3;

then ( x in X \/ Y or x in Z ) by XBOOLE_0:def 3;

hence x in (X \/ Y) \/ Z by XBOOLE_0:def 3; :: 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 x in (X \/ Y) \/ Z ; :: thesis: x in X \/ (Y \/ Z)

then ( x in X \/ Y or x in Z ) by XBOOLE_0:def 3;

then ( x in X or x in Y or x in Z ) by XBOOLE_0:def 3;

then ( x in X or x in Y \/ Z ) by XBOOLE_0:def 3;

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

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

then ( x in X \/ Y or x in Z ) by XBOOLE_0:def 3;

then ( x in X or x in Y or x in Z ) by XBOOLE_0:def 3;

then ( x in X or x in Y \/ Z ) by XBOOLE_0:def 3;

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

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

then ( x in X or x in Y \/ Z ) by XBOOLE_0:def 3;

then ( x in X or x in Y or x in Z ) by XBOOLE_0:def 3;

then ( x in X \/ Y or x in Z ) by XBOOLE_0:def 3;

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