theorem Th32: :: GTARSKI5:32

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
Plane (A,r) = { x where x is POINT of S : ( A out x,r or x in A or between r,A,x ) }