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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	inaglea.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	inaglea.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	inaglea.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	inaglea.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	inaglea.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	inaglea.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	inaglea.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	inaglea.1	⊢ ( 𝜑 → 𝐶 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑌 ”⟩ )
Assertion	inaglea	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑌 ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		inaglea.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		inaglea.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		inaglea.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
4		inaglea.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		inaglea.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		inaglea.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7		inaglea.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8		inaglea.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
9		inaglea.1	⊢ ( 𝜑 → 𝐶 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑌 ”⟩ )
10		eqid	⊢ ( ≤∠ ‘ 𝐺 ) = ( ≤∠ ‘ 𝐺 )
11	1 2 3 7 5 6 8 4 9	inagne1	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
12	1 2 3 7 5 6 8 4 9	inagne3	⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
13	12	necomd	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
14	1 2 4 3 5 6 7 11 13	cgraid	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
15	1 4 5 6 7 5 6 8 10 7 9 14	isleagd	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑌 ”⟩ )