---

Step * 2 of Lemma perp-in-congruence


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)
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 a ≠ b)⌝⋅ }

1
.....assertion..... 
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) supposing (ab  ⊥d dc and AB  ⊥D DC and bc ≅ BC and ac ≅ AC and ab ≅ AB and a ≠ b)

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)
2. ∀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 a ≠ b)
⊢ ∀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:

1.  \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)
\mvdash{}  \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 
                              a  \mneq{}  b)\mkleeneclose{}\mcdot{}

---

Home Index