let X be set ; :: thesis: ( not X is trivial implies not X is empty )
assume not X is trivial ; :: thesis: not X is empty
hence not X is empty ; :: thesis: verum