let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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; :: thesis: ( 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 ) ) ) :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: verum