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

thus X /\ {} c= {} by XBOOLE_0:def 4; :: 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 4; :: 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