df-lines2 - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-lines2		Structured version Visualization version Unicode version

Definition df-lines2 32246

Description: Define the set of all lines. Definition 6.14, part 2 of [Schwabhauser] p. 45. See ellines 32259 for membership. (Contributed by Scott Fenton, 28-Oct-2013.)

**Assertion**
Ref	Expression
df-lines2	LinesEE Line

**Detailed syntax breakdown of Definition df-lines2**
Step	Hyp	Ref	Expression
1		clines2 32243	. 2 LinesEE
2		cline2 32241	. . 3 Line
3	2	crn 5115	. 2 Line
4	1, 3	wceq 1483	1 LinesEE Line

Colors of variables: wff setvar class

This definition is referenced by: ellines 32259

W3C validator