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

thus ( X misses Y implies X \ Y = X ) :: thesis: ( X \ Y = X implies X misses Y )

for x being object holds not x in X /\ Y

thus ( X misses Y implies X \ Y = X ) :: thesis: ( X \ Y = X implies X misses Y )

proof

assume A2:
X \ Y = X
; :: thesis: X misses Y
assume A1:
X /\ Y = {}
; :: according to XBOOLE_0:def 7 :: thesis: X \ Y = X

thus for x being object st x in X \ Y holds

x in X by XBOOLE_0:def 5; :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: X c= X \ Y

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in X \ Y )

( x in X /\ Y or not x in X or not x in Y ) by XBOOLE_0:def 4;

hence ( not x in X or x in X \ Y ) by A1, XBOOLE_0:def 5; :: thesis: verum

end;thus for x being object st x in X \ Y holds

x in X by XBOOLE_0:def 5; :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: X c= X \ Y

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in X \ Y )

( x in X /\ Y or not x in X or not x in Y ) by XBOOLE_0:def 4;

hence ( not x in X or x in X \ Y ) by A1, XBOOLE_0:def 5; :: thesis: verum

for x being object holds not x in X /\ Y

proof

hence
X misses Y
by XBOOLE_0:4; :: thesis: verum
given x being object such that A3:
x in X /\ Y
; :: thesis: contradiction

( x in X & x in Y ) by A3, XBOOLE_0:def 4;

hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum

end;( x in X & x in Y ) by A3, XBOOLE_0:def 4;

hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum