---

Step * of Lemma sg-op-sep

∀sg:s-GroupStructure. ∀x1,y1,x2,y2:Point.  ((x1 y1) # (x2 y2) ⇒ (x1 # x2 ∨ y1 # y2))
BY
{ (Auto
   THEN D 1
   THEN Auto
   THEN All  (Fold `sg-op`)
   THEN (Assert ∀x,x',y,y':Point.  ((x y) # (x' y') ⇒ (x # x' ∨ y # y')) BY
               (UseWitness ⌜sg."opsep"⌝⋅ THEN Trivial))
   THEN BHyp -1 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}sg:s-GroupStructure.  \mforall{}x1,y1,x2,y2:Point.    ((x1  y1)  \#  (x2  y2)  {}\mRightarrow{}  (x1  \#  x2  \mvee{}  y1  \#  y2))


By

---

Latex:
(Auto
  THEN  D  1
  THEN  Auto
  THEN  All    (Fold  `sg-op`)
  THEN  (Assert  \mforall{}x,x',y,y':Point.    ((x  y)  \#  (x'  y')  {}\mRightarrow{}  (x  \#  x'  \mvee{}  y  \#  y'))  BY
                          (UseWitness  \mkleeneopen{}sg."opsep"\mkleeneclose{}\mcdot{}  THEN  Trivial))
  THEN  BHyp  -1 
  THEN  Auto)

---

Home Index