let X be set ; :: thesis: {} \ X = {}
thus {} \ X c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= {} \ X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {} \ X or x in {} )
assume x in {} \ X ; :: thesis: x in {}
hence x in {} by XBOOLE_0:def 5; :: thesis: verum

end;

let x be set ; :: 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