let X be set ; :: thesis: {} \ X = {}

thus {} \ X c= {} by XBOOLE_0:def 5; :: according to XBOOLE_0:def 10 :: thesis: {} c= {} \ X

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

assume x in {} ; :: thesis: x in {} \ X

hence x in {} \ X by XBOOLE_0:def 1; :: thesis: verum

thus {} \ X c= {} by XBOOLE_0:def 5; :: according to XBOOLE_0:def 10 :: thesis: {} c= {} \ X

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

assume x in {} ; :: thesis: x in {} \ X

hence x in {} \ X by XBOOLE_0:def 1; :: thesis: verum