let X be set ; :: thesis: ( X c= {} implies X = {} )

assume X c= {} ; :: thesis: X = {}

hence ( X c= {} & {} c= X ) ; :: according to XBOOLE_0:def 10 :: thesis: verum

assume X c= {} ; :: thesis: X = {}

hence ( X c= {} & {} c= X ) ; :: according to XBOOLE_0:def 10 :: thesis: verum