Step
*
4
1
of Lemma
lsep-opposite-iff
1. g : OrientedPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ab
7. y leftof ba
8. x leftof ab
⇐ y leftof ba
9. y leftof ba
10. x1 : Point
11. Colinear(a;b;x1)
12. x_x1_y
⊢ Colinear(x1;a;b)
BY
{ ((All (RWO "not-lsep-iff-colinear<") THENA Auto) THEN ParallelOp -2 THEN EAuto 2) }
Latex:
Latex:
1. g : OrientedPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ab
7. y leftof ba
8. x leftof ab \mLeftarrow{}{} y leftof ba
9. y leftof ba
10. x1 : Point
11. Colinear(a;b;x1)
12. x\_x1\_y
\mvdash{} Colinear(x1;a;b)
By
Latex:
((All (RWO "not-lsep-iff-colinear<") THENA Auto) THEN ParallelOp -2 THEN EAuto 2)
Home
Index