Theorem lnssplng1

Description: A line defined by two points X and Y , both on a plane H , is entirely contained in H . First part of Theorem 9.25 of Schwabhauser p. 75. (Contributed by Thierry Arnoux, 17-Jun-2026)

	Ref	Expression
Hypotheses	plngval.p	|- P = ( Base ` G )
	plngval.i	|- I = ( Itv ` G )
	plngval.1	|- L = ( LineG ` G )
	plngval.e	|- E = ( PlnG ` G )
	plngval.g	|- ( ph -> G e. TarskiG )
	lnssplng.h	|- ( ph -> H e. ran E )
	lnssplng.x	|- ( ph -> X e. H )
	lnssplng.y	|- ( ph -> Y e. H )
	lnssplng.1	|- ( ph -> X =/= Y )
Assertion	lnssplng1	|- ( ph -> ( X L Y ) C_ H )

Proof

Step	Hyp	Ref	Expression
1		plngval.p	|- P = ( Base ` G )
2		plngval.i	|- I = ( Itv ` G )
3		plngval.1	|- L = ( LineG ` G )
4		plngval.e	|- E = ( PlnG ` G )
5		plngval.g	|- ( ph -> G e. TarskiG )
6		lnssplng.h	|- ( ph -> H e. ran E )
7		lnssplng.x	|- ( ph -> X e. H )
8		lnssplng.y	|- ( ph -> Y e. H )
9		lnssplng.1	|- ( ph -> X =/= Y )
10	1 2 3 4 5 6 7 8 9	lnssplng	|- ( ph -> ( ( X L Y ) C_ H /\ E. s e. ( P \ ( X L Y ) ) H = ( ( X L Y ) E s ) ) )
11	10	simpld	|- ( ph -> ( X L Y ) C_ H )