let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, p being POINT of S
for A being Subset of S st A is_line & p in A & Collinear a,b,p holds
( A out a,b iff ( p out a,b & not a in A ) )
let a, b, p be POINT of S; :: thesis: for A being Subset of S st A is_line & p in A & Collinear a,b,p holds
( A out a,b iff ( p out a,b & not a in A ) )
let A be Subset of S; :: thesis: ( A is_line & p in A & Collinear a,b,p implies ( A out a,b iff ( p out a,b & not a in A ) ) )
assume that
A1: A is_line and
A2: p in A and
A3: Collinear a,b,p ; :: thesis: ( A out a,b iff ( p out a,b & not a in A ) )

hereby :: thesis: ( p out a,b & not a in A implies A out a,b )

assume A4: A out a,b ; :: thesis: ( p out a,b & not a in A )
consider c being POINT of S such that
A5: between a,A,c and
A6: between b,A,c by A4;
A7: Collinear a,p,b by A3, GTARSKI3:45;
not between a,p,b

proof

assume between a,p,b ; :: thesis: contradiction
then between a,A,b by A2, A5, A6;
hence contradiction by Th15, A4; :: thesis: verum

end;

hence p out a,b by A7, GTARSKI3:73; :: thesis: not a in A
thus not a in A by A5; :: thesis: verum

end;

assume that
A8: p out a,b and
A9: not a in A ; :: thesis: A out a,b
set c = reflection (p,a);
( between b,A, reflection (p,a) iff A out a,b ) by A1, A2, A8, A9, Th28, Th27;
hence A out a,b by A1, A2, A8, A9, Th27; :: thesis: verum