Theorem inagflat

Description: Any point lies in a flat angle. (Contributed by Thierry Arnoux, 13-Feb-2023)

	Ref	Expression
Hypotheses	isinag.p	$$⊢P={\mathrm{Base}}_G$$
	isinag.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	isinag.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
	isinag.x	$$⊢\phi \to X\in P$$
	isinag.a	$$⊢\phi \to A\in P$$
	isinag.b	$$⊢\phi \to B\in P$$
	isinag.c	$$⊢\phi \to C\in P$$
	inagflat.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	inagflat.x	$$⊢\phi \to X\in P$$
	inagflat.1	$$⊢\phi \to A\ne B$$
	inagflat.2	$$⊢\phi \to C\ne B$$
	inagflat.3	$$⊢\phi \to X\ne B$$
	inagflat.4	$$⊢\phi \to B\in \left(AIC\right)$$
Assertion	inagflat	$$⊢\phi \to X{\in }_{𝒢}^{\angle }\left(G\right)⟨“ABC”⟩$$

Proof

Step	Hyp	Ref	Expression
1		isinag.p	$$⊢P={\mathrm{Base}}_G$$
2		isinag.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
3		isinag.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
4		isinag.x	$$⊢\phi \to X\in P$$
5		isinag.a	$$⊢\phi \to A\in P$$
6		isinag.b	$$⊢\phi \to B\in P$$
7		isinag.c	$$⊢\phi \to C\in P$$
8		inagflat.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
9		inagflat.x	$$⊢\phi \to X\in P$$
10		inagflat.1	$$⊢\phi \to A\ne B$$
11		inagflat.2	$$⊢\phi \to C\ne B$$
12		inagflat.3	$$⊢\phi \to X\ne B$$
13		inagflat.4	$$⊢\phi \to B\in \left(AIC\right)$$
14		eqidd	$$⊢\phi \to B=B$$
15	14	orcd	$$⊢\phi \to \left(B=B\vee BK\left(B\right)X\right)$$
16	1 2 3 4 5 6 7 8 6 10 11 12 13 15	isinagd	$$⊢\phi \to X{\in }_{𝒢}^{\angle }\left(G\right)⟨“ABC”⟩$$