Description: Define the set of all lines. Definition 6.14, part 2 of Schwabhauser p. 45. See ellines for membership. (Contributed by Scott Fenton, 28-Oct-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-lines2 | ⊢ LinesEE = ran Line |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | clines2 | ⊢ LinesEE | |
| 1 | cline2 | ⊢ Line | |
| 2 | 1 | crn | ⊢ ran Line |
| 3 | 0 2 | wceq | ⊢ LinesEE = ran Line |