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

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