equal
deleted
inserted
replaced
422 |
422 |
423 (*Lemma for the trivial direction of the if-and-only-if*) |
423 (*Lemma for the trivial direction of the if-and-only-if*) |
424 goal thy |
424 goal thy |
425 "!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H) ==> \ |
425 "!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H) ==> \ |
426 \ (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)"; |
426 \ (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)"; |
427 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1); |
427 by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1); |
428 qed "analz_image_freshK_lemma"; |
428 qed "analz_image_freshK_lemma"; |