equal
deleted
inserted
replaced
32 let ?S = "{x. x ~: f x}" |
32 let ?S = "{x. x ~: f x}" |
33 show "?S ~: range f" |
33 show "?S ~: range f" |
34 proof |
34 proof |
35 assume "?S : range f" |
35 assume "?S : range f" |
36 then obtain y where "?S = f y" .. |
36 then obtain y where "?S = f y" .. |
37 thus False |
37 then show False |
38 proof (rule equalityCE) |
38 proof (rule equalityCE) |
39 assume "y : f y" |
39 assume "y : f y" |
40 assume "y : ?S" hence "y ~: f y" .. |
40 assume "y : ?S" then have "y ~: f y" .. |
41 thus ?thesis by contradiction |
41 with `y : f y` show ?thesis by contradiction |
42 next |
42 next |
43 assume "y ~: ?S" |
43 assume "y ~: ?S" |
44 assume "y ~: f y" hence "y : ?S" .. |
44 assume "y ~: f y" then have "y : ?S" .. |
45 thus ?thesis by contradiction |
45 with `y ~: ?S` show ?thesis by contradiction |
46 qed |
46 qed |
47 qed |
47 qed |
48 qed |
48 qed |
49 |
49 |
50 text {* |
50 text {* |