(* -------------------------------------------------------------------------- *)
ntheorem prove_these_axioms_3:
(* -------------------------------------------------------------------------- *)
ntheorem prove_these_axioms_3:
∀H0:∀A:Univ.eq Univ identity (divide A A).
∀H1:∀A:Univ.∀B:Univ.eq Univ (inverse A) (divide (divide B B) A).
∀H2:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (multiply A B) (divide A (divide (divide C C) B)).
∀H0:∀A:Univ.eq Univ identity (divide A A).
∀H1:∀A:Univ.∀B:Univ.eq Univ (inverse A) (divide (divide B B) A).
∀H2:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (multiply A B) (divide A (divide (divide C C) B)).