new theorem subset_Compl_self_eq

--- a/src/HOL/equalities.ML	Thu Jan 13 15:29:52 2000 +0100
+++ b/src/HOL/equalities.ML	Thu Jan 13 17:29:04 2000 +0100
@@ -401,8 +401,11 @@
 
 Addsimps [Compl_Un, Compl_Int, Compl_UN, Compl_INT];
 
+Goal "(A <= -A) = (A = {})";
+by (Blast_tac 1);
+qed "subset_Compl_self_eq";
+
 (*Halmos, Naive Set Theory, page 16.*)
-
 Goal "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
 by (blast_tac (claset() addSEs [equalityCE]) 1);
 qed "Un_Int_assoc_eq";