Definition df-lng

Description: Define the line index extractor for geometries. (Contributed by Thierry Arnoux, 27-Mar-2019)

	Ref	Expression
Assertion	df-lng	⊢ LineG = Slot ; 1 7

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clng	⊢ LineG
1		c1	⊢ 1
2		c7	⊢ 7
3	1 2	cdc	⊢ ; 1 7
4	3	cslot	⊢ Slot ; 1 7
5	0 4	wceq	⊢ LineG = Slot ; 1 7