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	|- LinesEE = ran Line

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clines2	|- LinesEE
1		cline2	|- Line
2	1	crn	|- ran Line
3	0 2	wceq	|- LinesEE = ran Line