Theorem inaglea

Description: If C lies inside angle <" A B Y "> , then angle <" A B C "> is less than or equal to <" A B Y "> . (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	inaglea.p	$$⊢P={\mathrm{Base}}_G$$
	inaglea.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	inaglea.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
	inaglea.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	inaglea.a	$$⊢\phi \to A\in P$$
	inaglea.b	$$⊢\phi \to B\in P$$
	inaglea.c	$$⊢\phi \to C\in P$$
	inaglea.y	$$⊢\phi \to Y\in P$$
	inaglea.1	$$⊢\phi \to C{\in }_{𝒢}^{\angle }\left(G\right)⟨“ABY”⟩$$
Assertion	inaglea	$$⊢\phi \to ⟨“ABC”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“ABY”⟩$$

Proof

Step	Hyp	Ref	Expression
1		inaglea.p	$$⊢P={\mathrm{Base}}_G$$
2		inaglea.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
3		inaglea.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
4		inaglea.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		inaglea.a	$$⊢\phi \to A\in P$$
6		inaglea.b	$$⊢\phi \to B\in P$$
7		inaglea.c	$$⊢\phi \to C\in P$$
8		inaglea.y	$$⊢\phi \to Y\in P$$
9		inaglea.1	$$⊢\phi \to C{\in }_{𝒢}^{\angle }\left(G\right)⟨“ABY”⟩$$
10		eqid	$$⊢{\le }_{𝒢}^{\angle }\left(G\right)={\le }_{𝒢}^{\angle }\left(G\right)$$
11	1 2 3 7 5 6 8 4 9	inagne1	$$⊢\phi \to A\ne B$$
12	1 2 3 7 5 6 8 4 9	inagne3	$$⊢\phi \to C\ne B$$
13	12	necomd	$$⊢\phi \to B\ne C$$
14	1 2 4 3 5 6 7 11 13	cgraid	$$⊢\phi \to ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ABC”⟩$$
15	1 4 5 6 7 5 6 8 10 7 9 14	isleagd	$$⊢\phi \to ⟨“ABC”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“ABY”⟩$$