Definition df-lines2

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	$$⊢\mathrm{LinesEE}=\mathrm{ran}\mathrm{Line}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clines2	$$class\mathrm{LinesEE}$$
1		cline2	$$class\mathrm{Line}$$
2	1	crn	$$class\mathrm{ran}\mathrm{Line}$$
3	0 2	wceq	$$wff\mathrm{LinesEE}=\mathrm{ran}\mathrm{Line}$$