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