equal
deleted
inserted
replaced
445 |
445 |
446 Goal "A : Pow(B) ==> A<=B"; |
446 Goal "A : Pow(B) ==> A<=B"; |
447 by (etac (Pow_iff RS iffD1) 1) ; |
447 by (etac (Pow_iff RS iffD1) 1) ; |
448 qed "PowD"; |
448 qed "PowD"; |
449 |
449 |
450 AddSIs [PowI]; |
450 AddIffs [Pow_iff]; |
451 AddSDs [PowD]; |
|
452 |
451 |
453 |
452 |
454 (*** Rules for the empty set ***) |
453 (*** Rules for the empty set ***) |
455 |
454 |
456 (*The set {x:0.False} is empty; by foundation it equals 0 |
455 (*The set {x:0.False} is empty; by foundation it equals 0 |