let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S
for A being Subset of S st between a,A,c holds
( between b,A,c iff A out a,b )
let a, b, c be POINT of S; :: thesis: for A being Subset of S st between a,A,c holds
( between b,A,c iff A out a,b )
let A be Subset of S; :: thesis: ( between a,A,c implies ( between b,A,c iff A out a,b ) )
assume A1: between a,A,c ; :: thesis: ( between b,A,c iff A out a,b )
hence ( between b,A,c implies A out a,b ) ; :: thesis: ( A out a,b implies between b,A,c )
assume A out a,b ; :: thesis: between b,A,c
then consider d being POINT of S such that
A2: between a,A,d and
A3: between b,A,d ;
consider x being POINT of S such that
A4: x in A and
A5: between a,x,d by A2;
consider y being POINT of S such that
A6: y in A and
A7: between b,y,d by A3;

per cases ( Collinear a,b,d or not Collinear a,b,d ) ;

suppose A8: Collinear a,b,d ; :: thesis: between b,A,c

A9: a <> d by A5, A4, A1, GTARSKI1:def 10;

per cases ( a = b or a <> b ) ;

suppose a = b ; :: thesis: between b,A,c

hence between b,A,c by A1; :: thesis: verum

end;

suppose A10: a <> b ; :: thesis: between b,A,c

T1: x in Line (a,b)

proof

d in { x where x is POINT of S : Collinear a,b,x } by A8;
then G1: Line (a,b) = Line (a,d) by A9, A10, GTARSKI3:82;
Collinear a,x,d by A5;
then Collinear a,d,x by GTARSKI3:45;
hence x in Line (a,b) by G1; :: thesis: verum

end;

T2: y in Line (a,b)

proof

T2: b <> d by A3, GTARSKI1:def 10;
Collinear b,a,d by A8, GTARSKI3:45;
then d in Line (b,a) ;
then H1: Line (a,b) = Line (b,d) by A10, T2, GTARSKI3:82;
Collinear b,y,d by A7;
then Collinear b,d,y by GTARSKI3:45;
hence y in Line (a,b) by H1; :: thesis: verum

end;

T3: A <> Line (a,b) by A1, GTARSKI3:83;
( Line (a,b) is_line & A is_line ) by A1, A10;
then x = y by T1, T2, T3, A4, A6, GTARSKI3:89;
then ( between d,x,a & between d,x,b ) by A7, A5, GTARSKI3:14;
then x out a,b by A2, A4, A3, GTARSKI3:57;
hence between b,A,c by A1, A4, Th12; :: thesis: verum

end;

end;

end;

suppose A11: not Collinear a,b,d ; :: thesis: between b,A,c

consider z being POINT of S such that
A12: between x,z,b and
A13: between y,z,a by A5, A7, GTARSKI1:def 11;
A14: x <> y

proof

assume x = y ; :: thesis: contradiction
then ( between d,x,a & between d,x,b ) by A5, A7, GTARSKI3:14;
then ( Collinear d,a,b or Collinear d,b,a ) by A2, A4, GTARSKI3:56;
hence contradiction by A11, GTARSKI3:45; :: thesis: verum

end;

then A15: Line (x,y) = A by A1, A4, A6, GTARSKI3:87;
y <> z

proof

assume y = z ; :: thesis: contradiction
then Collinear x,y,b by A12;
hence contradiction by A3, A15; :: thesis: verum

end;

then A16: y out a,z by A13, A6, A1;
T1: x <> z

proof

assume x = z ; :: thesis: contradiction
then Collinear y,x,a by A13;
then a in Line (y,x) ;
hence contradiction by A1, A14, A4, A6, GTARSKI3:87; :: thesis: verum

end;

A17: x out z,b by T1, A12, A4, A3;
between z,A,c by A16, A1, A6, Th12;
hence between b,A,c by A17, A4, Th12; :: thesis: verum

end;

end;