nle_antisym

Theorem. nle_antisym
a ∈ ℕ → b ∈ ℕ → a ≤ b → b ≤ a → a = b

Proof
nle_antisym. ⊢ a ∈ ℕ → b ∈ ℕ → a ≤ b → b ≤ a → a = b,
  pred_ii_restr nat_incl_in_real rle_antisym.

Dependencies
The given proof depends on five axioms:
comp, eq_subst, radd_closed, real_is_set, rle_antisym.