theorem Th46: :: GTARSKI5:46

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for E being Subset of S st E is_plane & a in E & b in E & a <> b holds
( Line (a,b) c= E & ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) ) )