Step
*
of Lemma
rset-neg_wf
No Annotations
∀[A:Set(ℝ)]. (-(A) ∈ Set(ℝ))
BY
{ (RepUR ``rset rset-neg rset-member`` 0 THEN Auto THEN D -1 THEN MemTypeCD THEN All Reduce THEN Auto) }
1
1. A : ℝ ⟶ ℙ
2. ∀x,y:ℝ.  ((x = y) 
⇒ (A x) 
⇒ (A y))
3. x : ℝ
4. y : ℝ
5. x = y
6. A -(x)
⊢ A -(y)
Latex:
Latex:
No  Annotations
\mforall{}[A:Set(\mBbbR{})].  (-(A)  \mmember{}  Set(\mBbbR{}))
By
Latex:
(RepUR  ``rset  rset-neg  rset-member``  0  THEN  Auto  THEN  D  -1  THEN  MemTypeCD  THEN  All  Reduce  THEN  Auto)
Home
Index