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