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 = ( Base ` G )
	inaglea.i	|- I = ( Itv ` G )
	inaglea.k	|- K = ( hlG ` G )
	inaglea.g	|- ( ph -> G e. TarskiG )
	inaglea.a	|- ( ph -> A e. P )
	inaglea.b	|- ( ph -> B e. P )
	inaglea.c	|- ( ph -> C e. P )
	inaglea.y	|- ( ph -> Y e. P )
	inaglea.1	|- ( ph -> C ( inA ` G ) <" A B Y "> )
Assertion	inaglea	|- ( ph -> <" A B C "> ( leA ` G ) <" A B Y "> )

Proof

Step	Hyp	Ref	Expression
1		inaglea.p	|- P = ( Base ` G )
2		inaglea.i	|- I = ( Itv ` G )
3		inaglea.k	|- K = ( hlG ` G )
4		inaglea.g	|- ( ph -> G e. TarskiG )
5		inaglea.a	|- ( ph -> A e. P )
6		inaglea.b	|- ( ph -> B e. P )
7		inaglea.c	|- ( ph -> C e. P )
8		inaglea.y	|- ( ph -> Y e. P )
9		inaglea.1	|- ( ph -> C ( inA ` G ) <" A B Y "> )
10		eqid	|- ( leA ` G ) = ( leA ` G )
11	1 2 3 7 5 6 8 4 9	inagne1	|- ( ph -> A =/= B )
12	1 2 3 7 5 6 8 4 9	inagne3	|- ( ph -> C =/= B )
13	12	necomd	|- ( ph -> B =/= C )
14	1 2 4 3 5 6 7 11 13	cgraid	|- ( ph -> <" A B C "> ( cgrA ` G ) <" A B C "> )
15	1 4 5 6 7 5 6 8 10 7 9 14	isleagd	|- ( ph -> <" A B C "> ( leA ` G ) <" A B Y "> )