Theorem ile_antisym

Proof
ile_antisym. ⊢ a ∈ ℤ → b ∈ ℤ → a ≤ b → b ≤ a → a = b,
  pred_ii_restr int_incl_in_real rle_antisym.

Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, rle_antisym.