Theorem lnssplng1

Description: A line defined by two points X and Y , both on a plane H , is entirely contained in H . First part of Theorem 9.25 of Schwabhauser p. 75. (Contributed by Thierry Arnoux, 17-Jun-2026)

	Ref	Expression
Hypotheses	plngval.p	$$⊢P={\mathrm{Base}}_G$$
	plngval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	plngval.1	$$⊢L={Line}_{𝒢}\left(G\right)$$
	plngval.e	No typesetting found for |- E = ( PlnG ` G ) with typecode |-
	plngval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	lnssplng.h	$$⊢\phi \to H\in \mathrm{ran}E$$
	lnssplng.x	$$⊢\phi \to X\in H$$
	lnssplng.y	$$⊢\phi \to Y\in H$$
	lnssplng.1	$$⊢\phi \to X\ne Y$$
Assertion	lnssplng1	$$⊢\phi \to XLY\subseteq H$$

Proof

Step	Hyp	Ref	Expression
1		plngval.p	$$⊢P={\mathrm{Base}}_G$$
2		plngval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
3		plngval.1	$$⊢L={Line}_{𝒢}\left(G\right)$$
4		plngval.e	Could not format E = ( PlnG ` G ) : No typesetting found for |- E = ( PlnG ` G ) with typecode |-
5		plngval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
6		lnssplng.h	$$⊢\phi \to H\in \mathrm{ran}E$$
7		lnssplng.x	$$⊢\phi \to X\in H$$
8		lnssplng.y	$$⊢\phi \to Y\in H$$
9		lnssplng.1	$$⊢\phi \to X\ne Y$$
10	1 2 3 4 5 6 7 8 9	lnssplng	$$⊢\phi \to \left(XLY\subseteq H\wedge \exists s\in \left(P\setminus \left(XLY\right)\right)H=\left(XLY\right)Es\right)$$
11	10	simpld	$$⊢\phi \to XLY\subseteq H$$