Theorem tglnssp

Description: Lines are subset of the geometry base set. That is, lines are sets of points. (Contributed by Thierry Arnoux, 17-May-2019)

	Ref	Expression
Hypotheses	tglngval.p	$$⊢P={\mathrm{Base}}_G$$
	tglngval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	tglngval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tglngval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tglngval.x	$$⊢\phi \to X\in P$$
	tglngval.y	$$⊢\phi \to Y\in P$$
	tglngval.z	$$⊢\phi \to X\ne Y$$
Assertion	tglnssp	$$⊢\phi \to XLY\subseteq P$$

Proof

Step	Hyp	Ref	Expression
1		tglngval.p	$$⊢P={\mathrm{Base}}_G$$
2		tglngval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
3		tglngval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		tglngval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		tglngval.x	$$⊢\phi \to X\in P$$
6		tglngval.y	$$⊢\phi \to Y\in P$$
7		tglngval.z	$$⊢\phi \to X\ne Y$$
8	1 2 3 4 5 6 7	tglngval	$$⊢\phi \to XLY=\left\{z\in P|\left(z\in \left(XIY\right)\vee X\in \left(zIY\right)\vee Y\in \left(XIz\right)\right)\right\}$$
9		ssrab2	$$⊢\left\{z\in P|\left(z\in \left(XIY\right)\vee X\in \left(zIY\right)\vee Y\in \left(XIz\right)\right)\right\}\subseteq P$$
10	8 9	eqsstrdi	$$⊢\phi \to XLY\subseteq P$$