theorem Th31: :: GTARSKI5:31
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for r being POINT of S
for A being Subset of S st A is_line & not r in A holds
( A c= Plane (A,r) & r in Plane (A,r) )