take the carrier' of C ; :: thesis: ( the carrier' of C is Subset of the carrier' of C & not the carrier' of C is empty )
the carrier' of C c= the carrier' of C ;
hence ( the carrier' of C is Subset of the carrier' of C & not the carrier' of C is empty ) ; :: thesis: verum