notation "hvbox(A break ⊆ B)" with precedence 59
for @{ 'subseteq $A $B}.
-interpretation "Subseteq" 'subseteq A B =
- (cic:/matita/formal_topology/leq.con A B).
+interpretation "Subseteq" 'subseteq A B = (leq A B).
axiom leq_refl: ∀A. A ⊆ A.
axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.
theorem th8: ∀A. i (m (i A)) = i (m (i (c (i A)))). intros; auto. qed.
theorem th9: ∀A. i (c (m (c (i A)))) = i (m (i A)). intros; auto depth=4. qed.
-(* theorem th7: ∀A. i (m (i A)) = i (s (i A)). *)
\ No newline at end of file
+(* theorem th7: ∀A. i (m (i A)) = i (s (i A)). *)