let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b being POINT of S
for A being Subset of S st between a,A,b holds
b in Plane (A,a)
let a, b be POINT of S; :: thesis: for A being Subset of S st between a,A,b holds
b in Plane (A,a)
let A be Subset of S; :: thesis: ( between a,A,b implies b in Plane (A,a) )
assume A1: between a,A,b ; :: thesis: b in Plane (A,a)
then b in { x where x is POINT of S : ( A out x,a or x in A or between a,A,x ) } ;
hence b in Plane (A,a) by A1, Th32; :: thesis: verum