Step * of Lemma rset-neg_wf

No Annotations
[A:Set(ℝ)]. (-(A) ∈ Set(ℝ))
BY
(RepUR ``rset rset-neg rset-member`` THEN Auto THEN -1 THEN MemTypeCD THEN All Reduce THEN Auto) }

1
1. : ℝ ⟶ ℙ
2. ∀x,y:ℝ.  ((x y)  (A x)  (A y))
3. : ℝ
4. : ℝ
5. y
6. -(x)
⊢ -(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