let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, p being POINT of S holds
( p out a,b iff ( a <> p & b <> p & ex c being POINT of S st
( c <> p & between a,p,c & between b,p,c ) ) )
let a, b, p be POINT of S; ( p out a,b iff ( a <> p & b <> p & ex c being POINT of S st
( c <> p & between a,p,c & between b,p,c ) ) )
thus
( p out a,b implies ( a <> p & b <> p & ex c being POINT of S st
( c <> p & between a,p,c & between b,p,c ) ) )
( a <> p & b <> p & ex c being POINT of S st
( c <> p & between a,p,c & between b,p,c ) implies p out a,b )proof
assume A1:
p out a,
b
;
( a <> p & b <> p & ex c being POINT of S st
( c <> p & between a,p,c & between b,p,c ) )
consider c being
POINT of
S such that A2:
(
between a,
p,
c &
p,
c equiv p,
a )
by GTARSKI1:def 8;
A3:
p <> c
by A1, A2, Satz2p2, GTARSKI1:def 7;
A4:
(
between p,
a,
b implies ex
c being
POINT of
S st
(
c <> p &
between a,
p,
c &
between b,
p,
c ) )
proof
assume
between p,
a,
b
;
ex c being POINT of S st
( c <> p & between a,p,c & between b,p,c )
between b,
p,
c
by A1, A2, A3, Satz6p2;
hence
ex
c being
POINT of
S st
(
c <> p &
between a,
p,
c &
between b,
p,
c )
by A2, A3;
verum
end;
(
between p,
b,
a implies ex
c being
POINT of
S st
(
c <> p &
between a,
p,
c &
between b,
p,
c ) )
proof
assume
between p,
b,
a
;
ex c being POINT of S st
( c <> p & between a,p,c & between b,p,c )
between b,
p,
c
by A1, A2, A3, Satz6p2;
hence
ex
c being
POINT of
S st
(
c <> p &
between a,
p,
c &
between b,
p,
c )
by A2, A3;
verum
end;
hence
(
a <> p &
b <> p & ex
c being
POINT of
S st
(
c <> p &
between a,
p,
c &
between b,
p,
c ) )
by A1, A4;
verum
end;
thus
( a <> p & b <> p & ex c being POINT of S st
( c <> p & between a,p,c & between b,p,c ) implies p out a,b )
by Satz6p2; verum