---

Step * of Lemma congruence-implies-between

No Annotations
∀e:EuclideanPlane
  ∀[a,b,c,d,A,B,C,D:Point].
    (B(ABC)) supposing 
       ((A # B ⇒ C # B ⇒ (A leftof BD ⇐⇒ C leftof DB)) and 
       B(abc) and 
       d # b and 
       bd ≅ BD and 
       ad ≅ AD and 
       cd ≅ CD and 
       bc ≅ BC and 
       ab ≅ AB)
BY
{ Auto }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. A : Point
7. B : Point
8. C : Point
9. D : Point
10. ab ≅ AB
11. bc ≅ BC
12. cd ≅ CD
13. ad ≅ AD
14. bd ≅ BD
15. d # b
16. B(abc)
17. A # B ⇒ C # B ⇒ (A leftof BD ⇐⇒ C leftof DB)
⊢ B(ABC)

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane
    \mforall{}[a,b,c,d,A,B,C,D:Point].
        (B(ABC))  supposing 
              ((A  \#  B  {}\mRightarrow{}  C  \#  B  {}\mRightarrow{}  (A  leftof  BD  \mLeftarrow{}{}\mRightarrow{}  C  leftof  DB))  and 
              B(abc)  and 
              d  \#  b  and 
              bd  \mcong{}  BD  and 
              ad  \mcong{}  AD  and 
              cd  \mcong{}  CD  and 
              bc  \mcong{}  BC  and 
              ab  \mcong{}  AB)


By

---

Latex:
Auto

---

Home Index