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

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

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

A1: not x in {} by XBOOLE_0:def 1;

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

hence x in X \ {} by A1, XBOOLE_0:def 5; :: thesis: verum

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

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

A1: not x in {} by XBOOLE_0:def 1;

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

hence x in X \ {} by A1, XBOOLE_0:def 5; :: thesis: verum