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 out 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 out a,a
let A be Subset of S; :: thesis: ( A is_line & not a in A implies A out a,a )
assume ( A is_line & not a in A ) ; :: thesis: A out a,a
then ex c being POINT of S st between a,A,c by Th16;
hence A out a,a ; :: thesis: verum