let X, Y be set ; :: thesis: X \ Y c= X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ Y or x in X )
thus ( not x in X \ Y or x in X ) by XBOOLE_0:def 5; :: thesis: verum