theorem Th110: :: EUCLIDLP:110

for n being Nat
for x being Element of REAL n
for L0, L1, L2 being Element of line_of_REAL n
for P being Element of plane_of_REAL n st L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0 holds
( L0 c= P & L0 _|_ L1 )