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