let X, Y, Z be set ; :: thesis: ( X c= Z implies X \/ (Y /\ Z) = (X \/ Y) /\ Z )

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

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

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

x in Z by A4, XBOOLE_0:def 4;

then ( ( x in X & x in Z ) or x in Y /\ Z ) by A5, XBOOLE_0:def 4;

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

assume A1: X c= Z ; :: 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 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 A2: ( x in X or x in Y /\ Z ) by XBOOLE_0:def 3;

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

then A3: x in X \/ Y by XBOOLE_0:def 3;

x in Z by A1, A2, XBOOLE_0:def 4;

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

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

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

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

then A3: x in X \/ Y by XBOOLE_0:def 3;

x in Z by A1, A2, XBOOLE_0:def 4;

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

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

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

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

x in Z by A4, XBOOLE_0:def 4;

then ( ( x in X & x in Z ) or x in Y /\ Z ) by A5, XBOOLE_0:def 4;

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