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 between2 a,A,c holds
( between2 b,A,c iff A out2 a,b )
let a, b, c be POINT of S; :: thesis: for A being Subset of S st between2 a,A,c holds
( between2 b,A,c iff A out2 a,b )
let A be Subset of S; :: thesis: ( between2 a,A,c implies ( between2 b,A,c iff A out2 a,b ) )
assume A1: between2 a,A,c ; :: thesis: ( between2 b,A,c iff A out2 a,b )
hence ( between2 b,A,c implies A out2 a,b ) ; :: thesis: ( A out2 a,b implies between2 b,A,c )
assume A out2 a,b ; :: thesis: between2 b,A,c
then consider d being POINT of S such that
A2: between2 a,A,d and
A3: between2 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;
A is_plane by A2;
then consider p, q, r being POINT of S such that
A8: not Collinear p,q,r and
A9: A = Plane (p,q,r) ;

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

suppose A10: Collinear a,b,d ; :: thesis: between2 b,A,c

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

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

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

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

end;

suppose A12: a <> b ; :: thesis: between2 b,A,c

x = y

proof

assume A13: x <> y ; :: thesis: contradiction
W1: x in Line (a,b)

proof

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

end;

y in Line (a,b)

proof

T2: b <> d by A3, GTARSKI1:def 10;
Collinear b,a,d by A10, GTARSKI3:45;
then d in Line (b,a) ;
then H1: Line (a,b) = Line (b,d) by A12, 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;

then ( Line (x,y) = Line (a,b) & Line (x,y) c= Plane (p,q,r) ) by W1, A4, A6, A13, A12, A8, A9, GTARSKI4:11, Th69;
hence contradiction by A2, A9, GTARSKI3:83; :: thesis: verum

end;

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 between2 b,A,c by A1, A4, Th73; :: thesis: verum

end;

end;

end;

suppose A14: not Collinear a,b,d ; :: thesis: between2 b,A,c

consider z being POINT of S such that
A15: between x,z,b and
A16: between y,z,a by A5, A7, GTARSKI1:def 11;
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 A14, GTARSKI3:45; :: thesis: verum

end;

then A17: Line (x,y) c= A by A4, A6, A8, A9, Th69;
y <> z

proof

assume y = z ; :: thesis: contradiction
then Collinear x,y,b by A15;
then b in { t where t is POINT of S : Collinear x,y,t } ;
hence contradiction by A3, A17; :: thesis: verum

end;

then A18: y out a,z by A6, A1, A16;
G1: x <> z

proof

assume x = z ; :: thesis: contradiction
then Collinear y,x,a by A16;
then a in Line (y,x) ;
hence contradiction by A1, A17; :: thesis: verum

end;

A19: x out z,b by A4, A3, G1, A15;
between2 z,A,c by A18, A1, A6, Th73;
hence between2 b,A,c by A19, A4, Th73; :: thesis: verum

end;

end;