---

Step * of Lemma perp-in-congruence

∀e:EuclideanPlane
  ∀[a,b,A,B,c,d,C,D:Point].
    (ad ≅ AD ∧ bd ≅ BD ∧ cd ≅ CD) supposing (ab  ⊥d dc and AB  ⊥D DC and bc ≅ BC and ac ≅ AC and ab ≅ AB)
BY
{ Assert ⌜∀e:EuclideanPlane
            ∀[a,b,A,B,c,d,C,D:Point].
              (ad ≅ AD ∧ bd ≅ BD) supposing 
                 (ab  ⊥d dc and 
                 AB  ⊥D DC and 
                 bc ≅ BC and 
                 ac ≅ AC and 
                 ab ≅ AB and 
                 C # AB and 
                 c # ab)⌝⋅ }

1
.....assertion..... 
∀e:EuclideanPlane
  ∀[a,b,A,B,c,d,C,D:Point].
    (ad ≅ AD ∧ bd ≅ BD) supposing (ab  ⊥d dc and AB  ⊥D DC and bc ≅ BC and ac ≅ AC and ab ≅ AB and C # AB and c # ab)

2
1. ∀e:EuclideanPlane
     ∀[a,b,A,B,c,d,C,D:Point].
       (ad ≅ AD ∧ bd ≅ BD) supposing (ab  ⊥d dc and AB  ⊥D DC and bc ≅ BC and ac ≅ AC and ab ≅ AB and C # AB and c # ab)
⊢ ∀e:EuclideanPlane
    ∀[a,b,A,B,c,d,C,D:Point].
      (ad ≅ AD ∧ bd ≅ BD ∧ cd ≅ CD) supposing (ab  ⊥d dc and AB  ⊥D DC and bc ≅ BC and ac ≅ AC and ab ≅ AB)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane
    \mforall{}[a,b,A,B,c,d,C,D:Point].
        (ad  \mcong{}  AD  \mwedge{}  bd  \mcong{}  BD  \mwedge{}  cd  \mcong{}  CD)  supposing 
              (ab    \mbot{}d  dc  and 
              AB    \mbot{}D  DC  and 
              bc  \mcong{}  BC  and 
              ac  \mcong{}  AC  and 
              ab  \mcong{}  AB)


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}e:EuclideanPlane
                    \mforall{}[a,b,A,B,c,d,C,D:Point].
                        (ad  \mcong{}  AD  \mwedge{}  bd  \mcong{}  BD)  supposing 
                              (ab    \mbot{}d  dc  and 
                              AB    \mbot{}D  DC  and 
                              bc  \mcong{}  BC  and 
                              ac  \mcong{}  AC  and 
                              ab  \mcong{}  AB  and 
                              C  \#  AB  and 
                              c  \#  ab)\mkleeneclose{}\mcdot{}

---

Home Index