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

thus for x being object st x in (X \ Y) \ Z holds

x in X \ (Y \/ Z) :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: X \ (Y \/ Z) c= (X \ Y) \ Z

x in (X \ Y) \ Z :: according to TARSKI:def 3 :: thesis: verum

thus for x being object st x in (X \ Y) \ Z holds

x in X \ (Y \/ Z) :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: X \ (Y \/ Z) c= (X \ Y) \ Z

proof

thus
for x being object st x in X \ (Y \/ Z) holds
let x be object ; :: thesis: ( x in (X \ Y) \ Z implies x in X \ (Y \/ Z) )

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

then A2: not x in Z by XBOOLE_0:def 5;

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

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

not x in Y by A3, XBOOLE_0:def 5;

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

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

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

then A2: not x in Z by XBOOLE_0:def 5;

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

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

not x in Y by A3, XBOOLE_0:def 5;

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

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

x in (X \ Y) \ Z :: according to TARSKI:def 3 :: thesis: verum

proof

let x be object ; :: thesis: ( x in X \ (Y \/ Z) implies x in (X \ Y) \ Z )

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

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

then A7: not x in Y by XBOOLE_0:def 3;

A8: not x in Z by A6, XBOOLE_0:def 3;

x in X by A5, XBOOLE_0:def 5;

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

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

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

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

then A7: not x in Y by XBOOLE_0:def 3;

A8: not x in Z by A6, XBOOLE_0:def 3;

x in X by A5, XBOOLE_0:def 5;

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

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