Step
*
1
of Lemma
cong-angle-out-exists-iff
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. b ≠ a
9. b ≠ c
10. y ≠ x
11. y ≠ z
12. abc ≅a xyz
⊢ ∃a',c',x',z':Point. ((((out(b a'a) ∧ out(b c'c)) ∧ out(y x'x)) ∧ out(y z'z)) ∧ a'bc' ≅a x'yz')
BY
{ (FLemma `cong-angle-out-exists2` [-1] THEN Auto) }
1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. b ≠ a
9. b ≠ c
10. y ≠ x
11. y ≠ z
12. abc ≅a xyz
13. ∃a',c',x',z':Point. (out(b a'a) ∧ out(b c'c) ∧ out(y x'x) ∧ out(y z'z) ∧ a'bc' ≅a x'yz')
⊢ ∃a',c',x',z':Point. ((((out(b a'a) ∧ out(b c'c)) ∧ out(y x'x)) ∧ out(y z'z)) ∧ a'bc' ≅a x'yz')
Latex:
Latex:
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. b \mneq{} a
9. b \mneq{} c
10. y \mneq{} x
11. y \mneq{} z
12. abc \mcong{}\msuba{} xyz
\mvdash{} \mexists{}a',c',x',z':Point. ((((out(b a'a) \mwedge{} out(b c'c)) \mwedge{} out(y x'x)) \mwedge{} out(y z'z)) \mwedge{} a'bc' \mcong{}\msuba{} x'yz')
By
Latex:
(FLemma `cong-angle-out-exists2` [-1] THEN Auto)
Home
Index