diff options
Diffstat (limited to 'theories/Sets/Powerset.v')
| -rwxr-xr-x | theories/Sets/Powerset.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index 0db6c1012..9b2f57809 100755 --- a/theories/Sets/Powerset.v +++ b/theories/Sets/Powerset.v @@ -146,8 +146,8 @@ Theorem Union_is_Lub: Intros A a b H' H'0. Apply Lub_definition; Simpl. Apply Upper_Bound_definition; Simpl; Auto with sets. -(Intros y H'1; Elim H'1); Auto with sets. -(Intros y H'1; Elim H'1); Simpl; Auto with sets. +Intros y H'1; Elim H'1; Auto with sets. +Intros y H'1; Elim H'1; Simpl; Auto with sets. Qed. Theorem Intersection_is_Glb: @@ -162,8 +162,8 @@ Apply Glb_definition; Simpl. Apply Lower_Bound_definition; Simpl; Auto with sets. Apply Definition_of_Power_set. Generalize Inclusion_is_transitive; Intro IT; Red in IT; Apply IT with a; Auto with sets. -(Intros y H'1; Elim H'1); Auto with sets. -(Intros y H'1; Elim H'1); Simpl; Auto with sets. +Intros y H'1; Elim H'1; Auto with sets. +Intros y H'1; Elim H'1; Simpl; Auto with sets. Qed. End The_power_set_partial_order. |