---

Step * 1 of Lemma pgeo-lsep-implies-plsep-or


1. g : ProjectivePlane
2. p : Point
3. l : Line
4. m : Line
5. s : l ≠ m
6. s1 : p ≠ l ∧ m
7. a : Point
8. a I m
9. a ≠ l
10. p ≠ a
11. n : Line
12. p I n
13. l ∧ m ≠ n
⊢ p ≠ m ∨ p ≠ l
BY
{ (((InstLemma `pgeo-plsep-to-lsep` [⌜g⌝;⌜n⌝;⌜l⌝;⌜l ∧ m⌝]⋅ THEN Auto)
    THEN InstLemma `pgeo-plsep-to-lsep` [⌜g⌝;⌜n⌝;⌜m⌝;⌜l ∧ m⌝]⋅
    THEN Auto)
   THEN RenameVar `xx' (14)
   THEN RenameVar `t1\'' (15)
   THEN ((Assert m ≠ l BY EAuto 1 ) THEN RenameVar `s\'' (-1))
   THEN (Assert n ≠ l BY
               EAuto 1 )
   THEN RenameVar `t' (-1)) }

1
1. g : ProjectivePlane
2. p : Point
3. l : Line
4. m : Line
5. s : l ≠ m
6. s1 : p ≠ l ∧ m
7. a : Point
8. a I m
9. a ≠ l
10. p ≠ a
11. n : Line
12. p I n
13. l ∧ m ≠ n
14. xx : l ≠ n
15. t1' : m ≠ n
16. s' : m ≠ l
17. t : n ≠ l
⊢ p ≠ m ∨ p ≠ l

---

Latex:

---

Latex:

1.  g  :  ProjectivePlane
2.  p  :  Point
3.  l  :  Line
4.  m  :  Line
5.  s  :  l  \mneq{}  m
6.  s1  :  p  \mneq{}  l  \mwedge{}  m
7.  a  :  Point
8.  a  I  m
9.  a  \mneq{}  l
10.  p  \mneq{}  a
11.  n  :  Line
12.  p  I  n
13.  l  \mwedge{}  m  \mneq{}  n
\mvdash{}  p  \mneq{}  m  \mvee{}  p  \mneq{}  l


By

---

Latex:
(((InstLemma  `pgeo-plsep-to-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}l  \mwedge{}  m\mkleeneclose{}]\mcdot{}  THEN  Auto)
    THEN  InstLemma  `pgeo-plsep-to-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}l  \mwedge{}  m\mkleeneclose{}]\mcdot{}
    THEN  Auto)
  THEN  RenameVar  `xx'  (14)
  THEN  RenameVar  `t1\mbackslash{}''  (15)
  THEN  ((Assert  m  \mneq{}  l  BY  EAuto  1  )  THEN  RenameVar  `s\mbackslash{}''  (-1))
  THEN  (Assert  n  \mneq{}  l  BY
                          EAuto  1  )
  THEN  RenameVar  `t'  (-1))

---

Home Index