let X be set ; :: thesis: ( X <> {} implies {} c< X )
assume A1: X <> {} ; :: thesis: {} c< X
thus {} c= X ; :: according to XBOOLE_0:def 8 :: thesis: not {} = X
thus not {} = X by A1; :: thesis: verum