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

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

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

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

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

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

proof

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

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

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

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

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

hence x in X \ Y by A2, XBOOLE_0:def 5; :: thesis: verum

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

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

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

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

hence x in X \ Y by A2, XBOOLE_0:def 5; :: thesis: verum

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

proof

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

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

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

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

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

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

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

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

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

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

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