Step * of Lemma rv-sub-sep

rv:RealVectorSpace. ∀x,x',y,y':Point.  (x x' y'  (x x' ∨ y'))
BY
(Auto THEN Unfold `rv-sub` -1 THEN (FLemma `rv-add-sep` [-1] THENA Auto) THEN ParallelLast THEN Auto) }

1
1. rv RealVectorSpace
2. Point
3. x' Point
4. Point
5. y' Point
6. -y x' -y'
7. -y -y'
⊢ y'


Latex:


Latex:
\mforall{}rv:RealVectorSpace.  \mforall{}x,x',y,y':Point.    (x  -  y  \#  x'  -  y'  {}\mRightarrow{}  (x  \#  x'  \mvee{}  y  \#  y'))


By


Latex:
(Auto
  THEN  Unfold  `rv-sub`  -1
  THEN  (FLemma  `rv-add-sep`  [-1]  THENA  Auto)
  THEN  ParallelLast
  THEN  Auto)




Home Index