equal
deleted
inserted
replaced
32 from `lub A x` show "The (lub A) = x" |
32 from `lub A x` show "The (lub A) = x" |
33 proof |
33 proof |
34 fix x' assume lub': "lub A x'" |
34 fix x' assume lub': "lub A x'" |
35 show "x' = x" |
35 show "x' = x" |
36 proof (rule order_antisym) |
36 proof (rule order_antisym) |
37 from lub' show "x' \<le> x" |
37 from lub' show "x' \<le> x" |
38 proof |
38 proof |
39 fix a assume "a \<in> A" |
39 fix a assume "a \<in> A" |
40 then show "a \<le> x" .. |
40 then show "a \<le> x" .. |
41 qed |
41 qed |
42 show "x \<le> x'" |
42 show "x \<le> x'" |
43 proof |
43 proof |
44 fix a assume "a \<in> A" |
44 fix a assume "a \<in> A" |
45 with lub' show "a \<le> x'" .. |
45 with lub' show "a \<le> x'" .. |
46 qed |
46 qed |
47 qed |
47 qed |
48 qed |
48 qed |
49 qed |
49 qed |
50 qed |
50 qed |
51 |
51 |